1  /-
  2  Copyright (c) 2017 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Mario Carneiro
  5  -/
  6  import data.set.lattice data.set.finite
src         └──────────────┘ └─────────────┘
  7  import topology.instances.ennreal
src         └────────────────────────┘
  8         measure_theory.outer_measure
src         └──────────────────────────┘
  9  
 10  /-!
 11  # Measure spaces
 12  
 13  Measures are restricted to a measurable space (associated by the type class `measurable_space`).
 14  This allows us to prove equalities between measures by restricting to a generating set of the
 15  measurable space.
 16  
 17  On the other hand, the `μ.measure s` projection (i.e. the measure of `s` on the measure space `μ`)
 18  is the _outer_ measure generated by `μ`. This gives us a unrestricted monotonicity rule and it is
 19  somehow well-behaved on non-measurable sets.
 20  
 21  This allows us for the `lebesgue` measure space to have the `borel` measurable space, but still be
 22  a complete measure.
 23  -/
 24  
 25  noncomputable theory
 26  
 27  open classical set lattice filter finset function
 28  open_locale classical topological_space
 29  
 30  universes u v w x
 31  
 32  namespace measure_theory
 33  
 34  section of_measurable
 35  parameters {α : Type*} [measurable_space α]
id                           └──────────────┘
src                          └──────────────┘
typ                          └──────────────┘
 36  parameters (m : Π (s : set α), is_measurable s → ennreal)
id                          └─┘     └───────────┘    └─────┘
src                         └─┘     └───────────┘     └─────┘
typ                         └─┘     └───────────┘    └─────┘
doc                                 └───────────┘     └─────┘
 37  parameters (m0 : m ∅ is_measurable.empty = 0)
id                       └─────────────────┘ 
src                      └─────────────────┘ 
typ                      └─────────────────┘ 
 38  include m0
 39  
 40  /-- Measure projection which is ∞ for non-measurable sets.
 41  
 42  `measure'` is mainly used to derive the outer measure, for the main `measure` projection. -/
 43  def measure' (s : set α) : ennreal := ⨅ h : is_measurable s, m s h
id                     └─┘     └─────┘         └───────────┘    
src                    └─┘      └─────┘         └───────────┘  
typ                    └─┘     └─────┘         └───────────┘    
doc                             └─────┘         └───────────┘  
 44  
 45  lemma measure'_eq {s} (h : is_measurable s) : measure' s = m s h :=
id                              └───────────┘     └──────┘     
src                             └───────────┘      └──────┘   
typ                             └───────────┘     └──────┘     
doc                             └───────────┘      └──────┘
 46  by simp [measure', h]
id            └──────┘  
src     └────┘└──────┘└┘ └─
typ     └────┘└──────┘└┘└─
doc     └────┘└──────┘└┘ └─
txt     └────┘        └┘ └─
par     └────┘        └┘ └─
pid                 └┘ 
st        └────────────────
 47  
src  
typ  
doc  
txt  
par  
pid  
st   
 48  lemma measure'_empty : measure' ∅ = 0 :=
id                          └──────┘  
src                         └──────┘  
typ                         └──────┘  
doc                         └──────┘
 49  (measure'_eq is_measurable.empty).trans m0
id    └─────────┘ └─────────────────┘ └───┘  └┘
src   └─────────┘ └─────────────────┘ └───┘
typ   └─────────┘ └─────────────────┘ └───┘  └┘
 50  
 51  lemma measure'_Union_nat
 52    {f : ℕ → set α}
id             └─┘ 
src            └─┘
typ            └─┘ 
 53    (hm : ∀i, is_measurable (f i))
id              └───────────┘   
src              └───────────┘
typ             └───────────┘   
doc              └───────────┘
 54    (mU : m (⋃i, f i) (is_measurable.Union hm) = (∑i, m (f i) (hm i))) :
id                  └─────────────────┘ └┘           └┘ 
src                     └─────────────────┘        
typ                 └─────────────────┘ └┘           └┘ 
doc                                                 
 55    measure' (⋃i, f i) = (∑i, measure' (f i)) :=
id     └──────┘         └──────┘   
src    └──────┘             └──────┘
typ    └──────┘         └──────┘   
doc    └──────┘              └──────┘
 56  (measure'_eq _).trans $ mU.trans $
id    └─────────┘   └───┘    └┘└────┘
src   └─────────┘   └───┘      └────┘
typ   └─────────┘   └───┘    └┘└────┘
 57  by congr; funext i; rw measure'_eq
id                          └─────────┘
src     └───┘  └──────┘  └─┘└─────────┘
typ     └───┘  └──────┘  └─┘└─────────┘
doc            └──────┘  └─┘           
txt     └───┘  └──────┘  └─┘           
par     └───┘  └──────┘  └─┘           
pid                  └┘               
st     └───────────────────┘└─────────┘
 58  
src  
typ  
doc  
txt  
par  
pid  
st   
 59  /-- outer measure of a measure -/
 60  def outer_measure' : outer_measure α :=
id                        └───────────┘ 
src                       └───────────┘
typ                       └───────────┘ 
 61  outer_measure.of_function measure' measure'_empty
id   └───────────────────────┘ └──────┘ └────────────┘
src  └───────────────────────┘ └──────┘ └────────────┘
typ  └───────────────────────┘ └──────┘ └────────────┘
doc  └───────────────────────┘ └──────┘
 62  
 63  lemma measure'_Union_le_tsum_nat'
 64    (mU : ∀ {f : ℕ → set α} (hm : ∀i, is_measurable (f i)),
id                    └─┘            └───────────┘   
src                    └─┘              └───────────┘
typ                   └─┘            └───────────┘   
doc                                      └───────────┘
 65      m (⋃i, f i) (is_measurable.Union hm) ≤ (∑i, m (f i) (hm i)))
id              └─────────────────┘ └┘           └┘ 
src                 └─────────────────┘        
typ             └─────────────────┘ └┘           └┘ 
doc                                             
 66    (s : ℕ → set α) :
id             └─┘ 
src            └─┘
typ            └─┘ 
 67    measure' (⋃i, s i) ≤ (∑i, measure' (s i)) :=
id     └──────┘         └──────┘   
src    └──────┘             └──────┘
typ    └──────┘         └──────┘   
doc    └──────┘              └──────┘
 68  begin
st   └─────
 69    by_cases h : ∀i, is_measurable (s i),
id                      └───────────┘  
src    └───────┘ └─┘  └───────────┘   
typ    └───────┘ └─┘  └───────────┘  
doc    └───────┘ └─┘  └───────────┘   
txt    └───────┘ └─┘                  
par    └───────┘ └─┘                  
pid             └─┘                  
st   ─────────────────────────────────────┘└─
 70    { rw [measure'_eq _ _ (is_measurable.Union h),
id           └─────────┘      └─────────────────┘ 
src      └──┘└─────────┘└───┘ └─────────────────┘ └──
typ      └──┘└─────────┘└───┘ └─────────────────┘└──
doc      └──┘           └───┘                     └──
txt      └──┘           └───┘                     └──
par      └──┘           └───┘                     └──
pid        └┘           └───┘                     └──
st   ───┘└─────────────────────────────────────────┘└─
 71          congr_arg tsum _], {apply mU h},
id           └───────┘ └──┘            └┘ 
src  ───────┘└───────┘└──┘└─┘   └────┘  
typ  ───────┘└───────┘└──┘└─┘   └────┘└┘
doc  ───────┘         └──┘└─┘   └────┘  
txt  ───────┘             └─┘   └────┘  
par  ───────┘             └─┘   └────┘  
pid  ───────┘             └─┘          
st   ───────────────────────┘└────────────┘└┘
 72      funext i, apply measure'_eq _ _ (h i) },
id                       └─────────┘       
src      └──────┘  └────┘└─────────┘└───┘   └┘
typ      └──────┘  └────┘└─────────┘└───┘ └┘
doc      └──────┘  └────┘           └───┘   └┘
txt      └──────┘  └────┘           └───┘   └┘
par      └──────┘  └────┘           └───┘   └┘
pid            └┘                  └───┘   
st   ───────────┘└────────────────────────────┘└┘
 73    { cases not_forall.1 h with i hi,
id             └────────┘   
src      └────┘└────────┘└─┘ └────────┘
typ      └────┘└────────┘└─┘└────────┘
doc      └────┘          └─┘ └────────┘
txt      └────┘          └─┘ └────────┘
par      └────┘          └─┘ └────────┘
pid                     └─┘ └────────┘
st   ─────────────────────────────────┘└─
 74      exact le_trans (le_infi $ λ h, hi.elim h) (ennreal.le_tsum i) }
id             └──────┘  └─────┘        └─────┘     └─────────────┘ 
src      └────┘└──────┘ └─────┘  └──┘└─────┘ └┘ └─────────────┘ └┘
typ      └────┘└──────┘ └─────┘  └──┘└─────┘ └┘ └─────────────┘└┘
doc      └────┘                  └──┘        └┘                 └┘
txt      └────┘                  └──┘        └┘                 └┘
par      └────┘                  └──┘        └┘                 └┘
pid                             └──┘        └┘                 
st   ─────────────────────────────────────────────────────────────────┘└─
 75  end
st   ──┘
 76  
 77  parameter (mU : ∀ {f : ℕ → set α} (hm : ∀i, is_measurable (f i)),
id                            └─┘             └───────────┘   
src                            └─┘              └───────────┘
typ                           └─┘             └───────────┘   
doc                                              └───────────┘
 78    pairwise (disjoint on f) →
id     └──────┘  └──────┘ └┘ 
src    └──────┘  └──────┘ └┘
typ    └──────┘  └──────┘ └┘ 
doc    └──────┘  └──────┘
 79    m (⋃i, f i) (is_measurable.Union hm) = (∑i, m (f i) (hm i)))
id             └─────────────────┘ └┘            └┘ 
src               └─────────────────┘        
typ            └─────────────────┘ └┘            └┘ 
doc                                           
 80  include mU
 81  
 82  lemma measure'_Union
 83    {β} [encodable β] {f : β → set α}
id          └───────┘           └─┘ 
src         └───────┘             └─┘
typ         └───────┘           └─┘ 
doc         └───────┘
 84    (hd : pairwise (disjoint on f)) (hm : ∀i, is_measurable (f i)) :
id           └──────┘  └──────┘ └┘             └───────────┘   
src          └──────┘  └──────┘ └┘               └───────────┘
typ          └──────┘  └──────┘ └┘             └───────────┘   
doc          └──────┘  └──────┘                  └───────────┘
 85    measure' (⋃i, f i) = (∑i, measure' (f i)) :=
id     └──────┘         └──────┘   
src    └──────┘             └──────┘
typ    └──────┘         └──────┘   
doc    └──────┘              └──────┘
 86  begin
st   └─────
 87    rw [encodable.Union_decode2, outer_measure.Union_aux],
id         └─────────────────────┘  └─────────────────────┘
src    └──┘└─────────────────────┘└┘└─────────────────────┘
typ    └──┘└─────────────────────┘└┘└─────────────────────┘
doc    └──┘                       └┘                       
txt    └──┘                       └┘                       
par    └──┘                       └┘                       
pid      └┘                       └┘                       
st   ────────────────────────────┘└───────────────────────┘└──
 88    { exact measure'_Union_nat _ _
id             └────────────────┘
src      └────┘└────────────────┘└────
typ      └────┘└────────────────┘└────
doc      └────┘                  └────
txt      └────┘                  └────
par      └────┘                  └────
pid                             └────
st   ───┘└────────────────────────────
 89        (λ n, encodable.Union_decode2_cases is_measurable.empty hm)
id               └───────────────────────────┘ └─────────────────┘ └┘
src  ─────┘  └──┘└───────────────────────────┘└─────────────────┘  └─
typ  ─────┘  └──┘└───────────────────────────┘└─────────────────┘└┘└─
doc  ─────┘  └──┘                                                  └─
txt  ─────┘  └──┘                                                  └─
par  ─────┘  └──┘                                                  └─
pid  ─────┘  └──┘                                                  └─
st   ──────────────────────────────────────────────────────────────────
 90        (mU _ (measurable_space.Union_decode2_disjoint_on hd)) },
id          └┘    └────────────────────────────────────────┘ └┘
src  ─────┘   └─┘ └────────────────────────────────────────┘  └─┘
typ  ─────┘ └┘└─┘ └────────────────────────────────────────┘└┘└─┘
doc  ─────┘   └─┘                                             └─┘
txt  ─────┘   └─┘                                             └─┘
par  ─────┘   └─┘                                             └─┘
pid  ─────┘   └─┘                                             └┘
st   ────────────────────────────────────────────────────────────┘└┘
 91    { apply measure'_empty },
id             └────────────┘
src      └────┘└────────────┘
typ      └────┘└────────────┘
doc      └────┘              
txt      └────┘              
par      └────┘              
pid                         
st   ────────────────────────┘└──
 92  end
st   ──┘
 93  
 94  lemma measure'_union {s₁ s₂ : set α}
id                                 └─┘ 
src                                └─┘
typ                                └─┘ 
 95    (hd : disjoint s₁ s₂) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
id           └──────┘ └┘ └┘        └───────────┘ └┘        └───────────┘ └┘
src          └──────┘              └───────────┘           └───────────┘
typ          └──────┘ └┘ └┘        └───────────┘ └┘        └───────────┘ └┘
doc          └──────┘              └───────────┘           └───────────┘
 96    measure' (s₁ ∪ s₂) = measure' s₁ + measure' s₂ :=
id     └──────┘  └┘  └┘   └──────┘ └┘  └──────┘ └┘
src    └──────┘           └──────┘     └──────┘
typ    └──────┘  └┘  └┘   └──────┘ └┘  └──────┘ └┘
doc    └──────┘             └──────┘      └──────┘
 97  begin
st   └─────
 98    rw [union_eq_Union, measure'_Union _ _ @mU
id         └────────────┘  └────────────┘      └┘
src    └──┘└────────────┘└┘└────────────┘└───┘   
typ    └──┘└────────────┘└┘└────────────┘└───┘ └┘
doc    └──┘              └┘              └───┘   
txt    └──┘              └┘              └───┘   
par    └──┘              └┘              └───┘   
pid      └┘              └┘              └───┘   
st   ───────────────────┘└────────────────────────
 99        (pairwise_disjoint_on_bool.2 hd) (bool.forall_bool.2 ⟨h₂, h₁⟩),
id          └───────────────────────┘   └┘   └──────────────┘    └┘  └┘
src  ─────┘ └───────────────────────┘└─┘  └┘ └──────────────┘└─┘   └┘  └───
typ  ─────┘ └───────────────────────┘└─┘└┘└┘ └──────────────┘└─┘ └┘└┘└┘└───
doc  ─────┘                          └─┘  └┘                 └─┘   └┘  └───
txt  ─────┘                          └─┘  └┘                 └─┘   └┘  └───
par  ─────┘                          └─┘  └┘                 └─┘   └┘  └───
pid  ─────┘                          └─┘  └┘                 └─┘   └┘  └───
st   ───────────────────────────────────────────────────────────────────┘└─
100      tsum_fintype],
id       └──────────┘
src  ───┘└──────────┘
typ  ───┘└──────────┘
doc  ───┘            
txt  ───┘            
par  ───┘            
pid  ───┘            
st   ───────────────┘└──
101    change _+_ = _, simp
id               
src    └──────┘└┘└┘  └───┘
typ    └──────┘└┘└┘  └───┘
doc    └──────┘ └┘ └┘  └───┘
txt    └──────┘ └┘ └┘  └───┘
par    └──────┘ └┘ └┘  └───┘
pid          └┘ └┘ └┘      
st   ───────────────┘└─────┘
102  end
st   └─┘
103  
104  lemma measure'_mono {s₁ s₂ : set α} (h₁ : is_measurable s₁) (hs : s₁ ⊆ s₂) :
id                                └─┘         └───────────┘ └┘        └┘  └┘
src                               └─┘          └───────────┘              
typ                               └─┘         └───────────┘ └┘        └┘  └┘
doc                                            └───────────┘
105    measure' s₁ ≤ measure' s₂ :=
id     └──────┘ └┘  └──────┘ └┘
src    └──────┘     └──────┘
typ    └──────┘ └┘  └──────┘ └┘
doc    └──────┘      └──────┘
106  le_infi $ λ h₂, begin
id   └─────┘     └┘
src  └─────┘
typ  └─────┘     └┘
st                   └─────
107    have := measure'_union _ _ @mU disjoint_diff h₁ (h₂.diff h₁),
id             └────────────┘      └┘ └───────────┘     └─────┘ └┘
src    └──────┘└────────────┘└───┘   └───────────┘   └─────┘  
typ    └──────┘└────────────┘└───┘ └┘└───────────┘   └─────┘└┘
doc    └──────┘              └───┘                            
txt    └──────┘              └───┘                            
par    └──────┘              └───┘                            
pid    └───┘└─┘              └───┘                            
st   ─────────────────────────────────────────────────────────────┘└─
108    rw union_diff_cancel hs at this,
id        └───────────────┘ └┘
src    └─┘└───────────────┘  └──────┘
typ    └─┘└───────────────┘└┘└──────┘
doc    └─┘                   └──────┘
txt    └─┘                   └──────┘
par    └─┘                   └──────┘
pid                         └──────┘
st   ────────────────────────────────┘└─
109    rw ← measure'_eq m m0 _,
id          └─────────┘  └┘
src    └───┘└─────────┘   └┘
typ    └───┘└─────────┘└┘└┘
doc    └───┘              └┘
txt    └───┘              └┘
par    └───┘              └┘
pid      └─┘              └┘
st   ────────────────────────┘└─
110    exact le_iff_exists_add.2 ⟨_, this⟩
id           └───────────────┘       └──┘
src    └────┘└───────────────┘└─┘ └─┘    └┘
typ    └────┘└───────────────┘└─┘ └─┘└──┘└┘
doc    └────┘                 └─┘ └─┘    └┘
txt    └────┘                 └─┘ └─┘    └┘
par    └────┘                 └─┘ └─┘    └┘
pid                          └─┘ └─┘    
st   ─────────────────────────────────────┘
111  end
st   └─┘
112  
113  lemma measure'_Union_le_tsum_nat : ∀ (s : ℕ → set α),
id                                               └─┘ 
src                                               └─┘
typ                                              └─┘ 
114    measure' (⋃i, s i) ≤ (∑i, measure' (s i)) :=
id     └──────┘         └──────┘   
src    └──────┘             └──────┘
typ    └──────┘         └──────┘   
doc    └──────┘              └──────┘
115  measure'_Union_le_tsum_nat' $ λ f h, begin
id   └─────────────────────────┘      
src  └─────────────────────────┘
typ  └─────────────────────────┘      
st                                        └─────
116    simp [Union_disjointed.symm] {single_pass := tt},
id                                                  └┘
src    └────┘                     └┘ └─────────────┘└┘
typ    └────┘└───────────────────┘└┘ └─────────────┘└┘
doc    └────┘                     └┘ └─────────────┘  
txt    └────┘                     └┘ └─────────────┘  
par    └────┘                     └┘ └─────────────┘  
pid                              └─────────────┘  
st   ─────────────────────────────────────────────────┘└─
117    rw [mU (is_measurable.disjointed h) disjoint_disjointed],
id         └┘  └──────────────────────┘   └─────────────────┘
src    └──┘   └──────────────────────┘ └┘└─────────────────┘
typ    └──┘└┘ └──────────────────────┘└┘└─────────────────┘
doc    └──┘                            └┘                   
txt    └──┘                            └┘                   
par    └──┘                            └┘                   
pid      └┘                            └┘                   
st   ────────────────────────────────────────────────────────┘└──
118    refine ennreal.tsum_le_tsum (λ i, _),
id            └──────────────────┘
src    └─────┘└──────────────────┘  └────┘
typ    └─────┘└──────────────────┘  └────┘
doc    └─────┘                      └────┘
txt    └─────┘                      └────┘
par    └─────┘                      └────┘
pid                                └────┘
st   ─────────────────────────────────────┘└─
119    rw [← measure'_eq m m0, ← measure'_eq m m0],
id           └─────────┘  └┘    └─────────┘  └┘
src    └────┘└─────────┘   └──┘└─────────┘   
typ    └────┘└─────────┘└┘└──┘└─────────┘└┘
doc    └────┘              └──┘              
txt    └────┘              └──┘              
par    └────┘              └──┘              
pid      └──┘              └──┘              
st   ───────────────────────┘└──────────────────┘└──
120    exact measure'_mono _ _ @mU (is_measurable.disjointed h _) (inter_subset_left _ _)
id           └───────────┘      └┘  └──────────────────────┘      └───────────────┘
src    └────┘└───────────┘└───┘    └──────────────────────┘ └──┘ └───────────────┘└────┘
typ    └────┘└───────────┘└───┘ └┘ └──────────────────────┘└──┘ └───────────────┘└────┘
doc    └────┘             └───┘                             └──┘                  └────┘
txt    └────┘             └───┘                             └──┘                  └────┘
par    └────┘             └───┘                             └──┘                  └────┘
pid                      └───┘                             └──┘                  └───┘
st   ────────────────────────────────────────────────────────────────────────────────────┘
121  end
st   └─┘
122  
123  lemma outer_measure'_eq {s : set α} (hs : is_measurable s) :
id                                └─┘         └───────────┘ 
src                               └─┘          └───────────┘
typ                               └─┘         └───────────┘ 
doc                                            └───────────┘
124    outer_measure' s = m s hs :=
id     └────────────┘     └┘
src    └────────────┘   
typ    └────────────┘     └┘
doc    └────────────┘
125  by rw ← measure'_eq m m0 hs; exact
id           └─────────┘  └┘ └┘
src     └───┘└─────────┘       └────┘
typ     └───┘└─────────┘└┘└┘  └────┘
doc     └───┘                  └────┘
txt     └───┘                  └────┘
par     └───┘                  └────┘
pid       └─┘                       
st     └────────────────────────────────
126  (le_antisymm (outer_measure.of_function_le _ _ _) $
id    └─────────┘  └──────────────────────────┘
src   └─────────┘ └──────────────────────────┘└──────┘ 
typ   └─────────┘ └──────────────────────────┘└──────┘ 
doc                                           └──────┘ 
txt                                           └──────┘ 
par                                           └──────┘ 
pid                                           └──────┘ 
st   ────────────────────────────────────────────────────
127    le_infi $ λ f, le_infi $ λ hf,
id                    └─────┘
src  ─┘         └──┘└─────┘  └────
typ  ─┘         └──┘└─────┘  └────
doc  ─┘         └──┘         └────
txt  ─┘         └──┘         └────
par  ─┘         └──┘         └────
pid  ─┘         └──┘         └────
st   ─────────────────────────────────
128    le_trans (measure'_mono _ _ @mU hs hf) $
id     └──────┘  └───────────┘      └┘ └┘
src  ─┘└──────┘ └───────────┘└───┘       └┘ 
typ  ─┘└──────┘ └───────────┘└───┘ └┘└┘  └┘ 
doc  ─┘                      └───┘       └┘ 
txt  ─┘                      └───┘       └┘ 
par  ─┘                      └───┘       └┘ 
pid  ─┘                      └───┘       └┘ 
st   ───────────────────────────────────────────
129    measure'_Union_le_tsum_nat _ _ @mU _)
id     └────────────────────────┘      └┘
src  ─┘└────────────────────────┘└───┘   └───
typ  ─┘└────────────────────────┘└───┘ └┘└───
doc  ─┘                          └───┘   └───
txt  ─┘                          └───┘   └───
par  ─┘                          └───┘   └───
pid  ─┘                          └───┘   └─┘
st   ────────────────────────────────────────
130  
src  
typ  
doc  
txt  
par  
pid  
st   
131  lemma outer_measure'_eq_measure' {s : set α} (hs : is_measurable s) :
id                                         └─┘         └───────────┘ 
src                                        └─┘          └───────────┘
typ                                        └─┘         └───────────┘ 
doc                                                     └───────────┘
132    outer_measure' s = measure' s :=
id     └────────────┘   └──────┘ 
src    └────────────┘    └──────┘
typ    └────────────┘   └──────┘ 
doc    └────────────┘     └──────┘
133  by rw [measure'_eq m m0 hs, outer_measure'_eq m m0 @mU hs]
id          └─────────┘  └┘ └┘  └───────────────┘  └┘  └┘ └┘
src     └──┘└─────────┘     └┘└───────────────┘        └─
typ     └──┘└─────────┘└┘└┘└┘└───────────────┘└┘ └┘└┘└─
doc     └──┘                └┘                         └─
txt     └──┘                └┘                         └─
par     └──┘                └┘                         └─
pid       └┘                └┘                         
st     └──────────────────────┘└─────────────────────────────┘
134  
src  
typ  
doc  
txt  
par  
pid  
st   
135  end of_measurable
136  
137  namespace outer_measure
138  variables {α : Type*} [measurable_space α] (m : outer_measure α)
id                         └──────────────┘         └───────────┘
src                         └──────────────┘         └───────────┘
typ                        └──────────────┘         └───────────┘
139  
140  def trim : outer_measure α :=
id              └───────────┘ 
src             └───────────┘
typ             └───────────┘ 
141  outer_measure' (λ s _, m s) m.empty
id   └────────────┘          └────┘
src  └────────────┘               └────┘
typ  └────────────┘          └────┘
doc  └────────────┘
142  
143  theorem trim_ge : m ≤ m.trim :=
id                       └───┘
src                        └───┘
typ                      └───┘
144  λ s, le_infi $ λ f, le_infi $ λ hs,
id       └─────┘       └─────┘     └┘
src       └─────┘        └─────┘
typ      └─────┘       └─────┘     └┘
145  le_trans (m.mono hs) $ le_trans (m.Union_nat f) $
id   └──────┘  └───┘ └┘    └──────┘  └────────┘ 
src  └──────┘   └───┘       └──────┘   └────────┘
typ  └──────┘  └───┘ └┘    └──────┘  └────────┘ 
146  ennreal.tsum_le_tsum $ λ i, le_infi $ λ hf, le_refl _
id   └──────────────────┘       └─────┘     └┘  └─────┘
src  └──────────────────┘        └─────┘         └─────┘
typ  └──────────────────┘       └─────┘     └┘  └─────┘
147  
148  theorem trim_eq {s : set α} (hs : is_measurable s) : m.trim s = m s :=
id                        └─┘         └───────────┘     └───┘    
src                       └─┘          └───────────┘       └───┘   
typ                       └─┘         └───────────┘     └───┘    
doc                                    └───────────┘
149  le_antisymm (le_trans (of_function_le _ _ _) (infi_le _ hs)) (trim_ge _ _)
id   └─────────┘  └──────┘  └────────────┘         └─────┘   └┘    └─────┘
src  └─────────┘  └──────┘  └────────────┘         └─────┘         └─────┘
typ  └─────────┘  └──────┘  └────────────┘         └─────┘   └┘    └─────┘
150  
151  theorem trim_congr {m₁ m₂ : outer_measure α}
id                               └───────────┘ 
src                              └───────────┘
typ                              └───────────┘ 
152    (H : ∀ {s : set α}, is_measurable s → m₁ s = m₂ s) :
id                 └─┘    └───────────┘    └┘   └┘ 
src                └─┘     └───────────┘          
typ                └─┘    └───────────┘    └┘   └┘ 
doc                        └───────────┘
153    m₁.trim = m₂.trim :=
id     └┘└───┘  └┘└───┘
src      └───┘    └───┘
typ    └┘└───┘  └┘└───┘
154  by unfold trim; congr; funext s hs; exact H hs
id                                              └┘
src     └─────────┘  └───┘  └─────────┘  └────┘   
typ     └─────────┘  └───┘  └─────────┘  └────┘└┘
doc     └─────────┘         └─────────┘  └────┘   
txt     └─────────┘  └───┘  └─────────┘  └────┘   
par     └─────────┘  └───┘  └─────────┘  └────┘   
pid           └───┘               └───┘          
st     └────────────────────────────────────────────
155  
src  
typ  
doc  
txt  
par  
pid  
st   
156  theorem trim_le_trim {m₁ m₂ : outer_measure α} (H : m₁ ≤ m₂) : m₁.trim ≤ m₂.trim :=
id                                 └───────────┘        └┘  └┘    └┘└───┘  └┘└───┘
src                                └───────────┘                     └───┘    └───┘
typ                                └───────────┘        └┘  └┘    └┘└───┘  └┘└───┘
157  λ s, infi_le_infi $ λ f, infi_le_infi $ λ hs,
id       └──────────┘       └──────────┘     └┘
src       └──────────┘        └──────────┘
typ      └──────────┘       └──────────┘     └┘
158  ennreal.tsum_le_tsum $ λ b, infi_le_infi $ λ hf, H _
id   └──────────────────┘       └──────────┘     └┘  
src  └──────────────────┘        └──────────┘
typ  └──────────────────┘       └──────────┘     └┘  
159  
160  theorem le_trim_iff {m₁ m₂ : outer_measure α} : m₁ ≤ m₂.trim ↔
id                                └───────────┘     └┘  └┘└───┘ 
src                               └───────────┘            └───┘ 
typ                               └───────────┘     └┘  └┘└───┘ 
161    ∀ s, is_measurable s → m₁ s ≤ m₂ s :=
id         └───────────┘    └┘   └┘ 
src         └───────────┘          
typ        └───────────┘    └┘   └┘ 
doc         └───────────┘
162  le_of_function.trans $ forall_congr $ λ s, le_infi_iff
id   └────────────┘└────┘   └──────────┘       └─────────┘
src  └────────────┘└────┘   └──────────┘        └─────────┘
typ  └────────────┘└────┘   └──────────┘       └─────────┘
163  
164  theorem trim_eq_infi (s : set α) : m.trim s = ⨅ t (st : s ⊆ t) (ht : is_measurable t), m t :=
id                             └─┘     └───┘                     └───────────┘    
src                            └─┘       └───┘                         └───────────┘   
typ                            └─┘     └───┘                     └───────────┘    
doc                                                                      └───────────┘   
165  begin
st   └─────
166    refine le_antisymm
id            └─────────┘
src    └─────┘└─────────┘
typ    └─────┘└─────────┘
doc    └─────┘           
txt    └─────┘           
par    └─────┘           
pid                     
st   ─────────────────────
167      (le_infi $ λ t, le_infi $ λ st, le_infi $ λ ht, _)
src  ───┘          └──┘         └───┘         └───────
typ  ───┘          └──┘         └───┘         └───────
doc  ───┘          └──┘         └───┘         └───────
txt  ───┘          └──┘         └───┘         └───────
par  ───┘          └──┘         └───┘         └───────
pid  ───┘          └──┘         └───┘         └───────
st   ───────────────────────────────────────────────────────
168      (le_infi $ λ f, le_infi $ λ hf, _),
id                       └─────┘
src  ───┘          └──┘└─────┘  └─────┘
typ  ───┘          └──┘└─────┘  └─────┘
doc  ───┘          └──┘         └─────┘
txt  ───┘          └──┘         └─────┘
par  ───┘          └──┘         └─────┘
pid  ───┘          └──┘         └─────┘
st   ─────────────────────────────────────┘└─
169    { rw ← trim_eq m ht, exact (trim m).mono st },
id            └─────┘  └┘         └──┘        └┘
src      └───┘└─────┘     └────┘ └──┘ └─────┘  
typ      └───┘└─────┘└┘  └────┘ └──┘└─────┘└┘
doc      └───┘            └────┘      └─────┘  
txt      └───┘            └────┘      └─────┘  
par      └───┘            └────┘      └─────┘  
pid        └─┘                       └─────┘  
st   ───┘└───────────────┘└───────────────────────┘└┘
170    { by_cases h : ∀i, is_measurable (f i),
id                        └───────────┘  
src      └───────┘ └─┘  └───────────┘   
typ      └───────┘ └─┘  └───────────┘  
doc      └───────┘ └─┘  └───────────┘   
txt      └───────┘ └─┘                  
par      └───────┘ └─┘                  
pid               └─┘                  
st   ───────────────────────────────────────┘└─
171      { refine infi_le_of_le _ (infi_le_of_le hf $
id                                               └┘
src        └─────┘             └─┘                 
typ        └─────┘             └─┘              └┘ 
doc        └─────┘             └─┘                 
txt        └─────┘             └─┘                 
par        └─────┘             └─┘                 
pid                           └─┘                 
st   ─────┘└──────────────────────────────────────────
172          infi_le_of_le (is_measurable.Union h) _),
id           └───────────┘  └─────────────────┘ 
src  ───────┘└───────────┘ └─────────────────┘ └──┘
typ  ───────┘└───────────┘ └─────────────────┘└──┘
doc  ───────┘                                  └──┘
txt  ───────┘                                  └──┘
par  ───────┘                                  └──┘
pid  ───────┘                                  └──┘
st   ───────────────────────────────────────────────┘└─
173        rw congr_arg tsum _, {exact m.Union_nat _},
id            └───────┘ └──┘           └─────────┘
src        └─┘└───────┘└──┘└┘   └────┘└─────────┘└┘
typ        └─┘└───────┘└──┘└┘   └────┘└─────────┘└┘
doc        └─┘         └──┘└┘   └────┘           └┘
txt        └─┘             └┘   └────┘           └┘
par        └─┘             └┘   └────┘           └┘
pid                       └┘                   └┘
st   ────────────────────────┘└────────────────────┘└┘
174        funext i, exact measure'_eq _ _ (h i) },
id                         └─────────┘       
src        └──────┘  └────┘└─────────┘└───┘   └┘
typ        └──────┘  └────┘└─────────┘└───┘ └┘
doc        └──────┘  └────┘           └───┘   └┘
txt        └──────┘  └────┘           └───┘   └┘
par        └──────┘  └────┘           └───┘   └┘
pid              └┘                  └───┘   
st   ─────────────┘└────────────────────────────┘└┘
175      { cases not_forall.1 h with i hi,
id               └────────┘   
src        └────┘└────────┘└─┘ └────────┘
typ        └────┘└────────┘└─┘└────────┘
doc        └────┘          └─┘ └────────┘
txt        └────┘          └─┘ └────────┘
par        └────┘          └─┘ └────────┘
pid                       └─┘ └────────┘
st   ───────────────────────────────────┘└─
176        exact le_trans (le_infi $ λ h, hi.elim h) (ennreal.le_tsum i) } }
id               └──────┘  └─────┘        └─────┘     └─────────────┘ 
src        └────┘└──────┘ └─────┘  └──┘└─────┘ └┘ └─────────────┘ └┘
typ        └────┘└──────┘ └─────┘  └──┘└─────┘ └┘ └─────────────┘└┘
doc        └────┘                  └──┘        └┘                 └┘
txt        └────┘                  └──┘        └┘                 └┘
par        └────┘                  └──┘        └┘                 └┘
pid                               └──┘        └┘                 
st   ───────────────────────────────────────────────────────────────────┘└───
177  end
st   ──┘
178  
179  theorem trim_eq_infi' (s : set α) : m.trim s = ⨅ t : {t // s ⊆ t ∧ is_measurable t}, m t.1 :=
id                              └─┘     └───┘                └───────────┘    
src                             └─┘       └───┘                    └───────────┘       
typ                             └─┘     └───┘                └───────────┘    
doc                                                                    └───────────┘   
180  by simp [infi_subtype, infi_and, trim_eq_infi]
id            └──────────┘  └──────┘  └──────────┘
src     └────┘└──────────┘└┘└──────┘└┘└──────────┘└─
typ     └────┘└──────────┘└┘└──────┘└┘└──────────┘└─
doc     └────┘            └┘        └┘            └─
txt     └────┘            └┘        └┘            └─
par     └────┘            └┘        └┘            └─
pid                     └┘        └┘            
st     └────────────────────────────────────────────
181  
src  
typ  
doc  
txt  
par  
pid  
st   
182  theorem trim_trim (m : outer_measure α) : m.trim.trim = m.trim :=
id                          └───────────┘     └────────┘  └───┘
src                         └───────────┘       └────────┘   └───┘
typ                         └───────────┘     └────────┘  └───┘
183  le_antisymm (le_trim_iff.2 $ λ s hs, by simp [trim_eq _ hs, le_refl]) (trim_ge _)
id   └─────────┘  └─────────┘       └┘           └─────┘   └┘  └─────┘    └─────┘
src  └─────────┘  └─────────┘               └────┘└─────┘└─┘  └┘└─────┘   └─────┘
typ  └─────────┘  └─────────┘       └┘     └────┘└─────┘└─┘└┘└┘└─────┘   └─────┘
doc                                          └────┘       └─┘  └┘       
txt                                          └────┘       └─┘  └┘       
par                                          └────┘       └─┘  └┘       
pid                                                     └─┘  └┘       
st                                          └───────────────────────────┘
184  
185  theorem trim_zero : (0 : outer_measure α).trim = 0 :=
id                            └───────────┘  └──┘  
src                           └───────────┘   └──┘  
typ                           └───────────┘  └──┘  
186  ext $ λ s, le_antisymm
id   └─┘       └─────────┘
src  └─┘        └─────────┘
typ  └─┘       └─────────┘
187    (le_trans ((trim 0).mono (subset_univ s)) $
id      └──────┘   └──┘   └──┘   └─────────┘ 
src     └──────┘   └──┘   └──┘   └─────────┘
typ     └──────┘   └──┘   └──┘   └─────────┘ 
188      le_of_eq $ trim_eq _ is_measurable.univ)
id       └──────┘   └─────┘   └────────────────┘
src      └──────┘   └─────┘   └────────────────┘
typ      └──────┘   └─────┘   └────────────────┘
189    (zero_le _)
id      └─────┘
src     └─────┘
typ     └─────┘
190  
191  theorem trim_add (m₁ m₂ : outer_measure α) : (m₁ + m₂).trim = m₁.trim + m₂.trim :=
id                             └───────────┘      └┘  └┘ └──┘   └┘└───┘  └┘└───┘
src                            └───────────┘              └──┘     └───┘    └───┘
typ                            └───────────┘      └┘  └┘ └──┘   └┘└───┘  └┘└───┘
192  ext $ λ s, begin
id   └─┘     
src  └─┘
typ  └─┘     
st              └─────
193    simp [trim_eq_infi'],
id           └───────────┘
src    └────┘└───────────┘
typ    └────┘└───────────┘
doc    └────┘             
txt    └────┘             
par    └────┘             
pid                     
st   ─────────────────────┘└─
194    rw ennreal.infi_add_infi,
id        └───────────────────┘
src    └─┘└───────────────────┘
typ    └─┘└───────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ─────────────────────────┘└─
195    rintro ⟨t₁, st₁, ht₁⟩ ⟨t₂, st₂, ht₂⟩,
src    └──────────────────────────────────┘
typ    └──────────────────────────────────┘
doc    └──────────────────────────────────┘
txt    └──────────────────────────────────┘
par    └──────────────────────────────────┘
pid          └────────────────────────────┘
st   ─────────────────────────────────────┘└─
196    exact ⟨⟨_, subset_inter_iff.2 ⟨st₁, st₂⟩, ht₁.inter ht₂⟩,
id                └──────────────┘    └─┘  └─┘   └───────┘ └─┘
src    └────┘  └─┘└──────────────┘└─┘    └┘   └─┘└───────┘   └──
typ    └────┘  └─┘└──────────────┘└─┘ └─┘└┘└─┘└─┘└───────┘└─┘└──
doc    └────┘  └─┘                └─┘    └┘   └─┘            └──
txt    └────┘  └─┘                └─┘    └┘   └─┘            └──
par    └────┘  └─┘                └─┘    └┘   └─┘            └──
pid           └─┘                └─┘    └┘   └─┘            └──
st   ────────────────────────────────────────────────────────────
197      add_le_add'
id       └─────────┘
src  ───┘└─────────┘
typ  ───┘└─────────┘
doc  ───┘           
txt  ───┘           
par  ───┘           
pid  ───┘           
st   ────────────────
198        (m₁.mono' (inter_subset_left _ _))
id          └──────┘  └───────────────┘
src  ─────┘ └──────┘ └───────────────┘└──────
typ  ─────┘ └──────┘ └───────────────┘└──────
doc  ─────┘                           └──────
txt  ─────┘                           └──────
par  ─────┘                           └──────
pid  ─────┘                           └──────
st   ─────────────────────────────────────────
199        (m₂.mono' (inter_subset_right _ _))⟩,
id          └──────┘  └────────────────┘
src  ─────┘ └──────┘ └────────────────┘└─────┘
typ  ─────┘ └──────┘ └────────────────┘└─────┘
doc  ─────┘                            └─────┘
txt  ─────┘                            └─────┘
par  ─────┘                            └─────┘
pid  ─────┘                            └─────┘
st   ─────────────────────────────────────────┘└─
200  end
st   ──┘
201  
202  theorem trim_sum_ge {ι} (m : ι → outer_measure α) : sum (λ i, (m i).trim) ≤ (sum m).trim :=
id                                   └───────────┘     └─┘         └──┘     └─┘  └──┘
src                                   └───────────┘      └─┘            └──┘     └─┘   └──┘
typ                                  └───────────┘     └─┘         └──┘     └─┘  └──┘
203  λ s, by simp [trim_eq_infi]; exact
id                └──────────┘
src          └────┘└──────────┘  └────┘
typ         └────┘└──────────┘  └────┘
doc          └────┘              └────┘
txt          └────┘              └────┘
par          └────┘              └────┘
pid                                 
st          └───────────────────────────
204  λ t st ht, ennreal.tsum_le_tsum (λ i,
id              └──────────────────┘
src   └────────┘└──────────────────┘  └───
typ   └────────┘└──────────────────┘  └───
doc   └────────┘                      └───
txt   └────────┘                      └───
par   └────────┘                      └───
pid   └────────┘                      └───
st   ──────────────────────────────────────
205    infi_le_of_le t $ infi_le_of_le st $ infi_le _ ht)
id                       └───────────┘      └─────┘
src  ─┘               └───────────┘   └─────┘└─┘  └─
typ  ─┘               └───────────┘   └─────┘└─┘  └─
doc  ─┘                                      └─┘  └─
txt  ─┘                                      └─┘  └─
par  ─┘                                      └─┘  └─
pid  ─┘                                      └─┘  
st   ─────────────────────────────────────────────────────
206  
src  
typ  
doc  
txt  
par  
pid  
st   
207  end outer_measure
208  
209  structure measure (α : Type*) [measurable_space α] extends outer_measure α :=
id                          └───┘   └──────────────┘           └───────────┘ 
src                                 └──────────────┘            └───────────┘
typ                         └───┘   └──────────────┘           └───────────┘ 
210  (m_Union {f : ℕ → set α} :
id                   └─┘ 
src                   └─┘
typ                  └─┘ 
211    (∀i, is_measurable (f i)) → pairwise (disjoint on f) →
id         └───────────┘        └──────┘  └──────┘ └┘ 
src         └───────────┘          └──────┘  └──────┘ └┘
typ        └───────────┘        └──────┘  └──────┘ └┘ 
doc         └───────────┘          └──────┘  └──────┘
212    measure_of (⋃i, f i) = (∑i, measure_of (f i)))
id     └────────┘         └────────┘   
src                          
typ    └────────┘         └────────┘   
doc                           
213  (trimmed : to_outer_measure.trim = to_outer_measure)
id              └──────────────┘└───┘  └──────────────┘
src                             └───┘ 
typ             └──────────────┘└───┘  └──────────────┘
214  
215  /-- Measure projections for a measure space.
216  
217  For measurable sets this returns the measure assigned by the `measure_of` field in `measure`.
218  But we can extend this to _all_ sets, but using the outer measure. This gives us monotonicity and
219  subadditivity for all sets.
220  -/
221  instance measure.has_coe_to_fun {α} [measurable_space α] : has_coe_to_fun (measure α) :=
id                                        └──────────────┘     └────────────┘  └─────┘ 
src                                       └──────────────┘      └────────────┘  └─────┘
typ                                       └──────────────┘     └────────────┘  └─────┘ 
222  ⟨λ _, set α → ennreal, λ m, m.to_outer_measure⟩
id        └─┘    └─────┘      └───────────────┘
src        └─┘     └─────┘        └───────────────┘
typ       └─┘    └─────┘      └───────────────┘
doc                └─────┘
223  
224  namespace measure
225  
226  def of_measurable {α} [measurable_space α]
id                          └──────────────┘ 
src                         └──────────────┘
typ                         └──────────────┘ 
227    (m : Π (s : set α), is_measurable s → ennreal)
id                 └─┘    └───────────┘    └─────┘
src                └─┘     └───────────┘     └─────┘
typ                └─┘    └───────────┘    └─────┘
doc                        └───────────┘     └─────┘
228    (m0 : m ∅ is_measurable.empty = 0)
id             └─────────────────┘ 
src             └─────────────────┘ 
typ            └─────────────────┘ 
229    (mU : ∀ {f : ℕ → set α} (h : ∀i, is_measurable (f i)),
id                    └─┘           └───────────┘   
src                    └─┘             └───────────┘
typ                   └─┘           └───────────┘   
doc                                     └───────────┘
230      pairwise (disjoint on f) →
id       └──────┘  └──────┘ └┘ 
src      └──────┘  └──────┘ └┘
typ      └──────┘  └──────┘ └┘ 
doc      └──────┘  └──────┘
231      m (⋃i, f i) (is_measurable.Union h) = (∑i, m (f i) (h i))) :
id              └─────────────────┘             
src                 └─────────────────┘       
typ             └─────────────────┘             
doc                                            
232    measure α :=
id     └─────┘ 
src    └─────┘
typ    └─────┘ 
233  { m_Union := λ f hf hd,
id                   └┘ └┘
typ                  └┘ └┘
234    show outer_measure' m m0 (Union f) =
id          └────────────┘  └┘  └───┘   
src         └────────────┘       └───┘    
typ         └────────────┘  └┘  └───┘   
doc         └────────────┘       └───┘
235        ∑ i, outer_measure' m m0 (f i), begin
id           └────────────┘  └┘   
src           └────────────┘
typ          └────────────┘  └┘   
doc           └────────────┘
st                                         └─────
236      rw [outer_measure'_eq m m0 @mU, mU hf hd],
id           └───────────────┘  └┘  └┘  └┘ └┘ └┘
src      └──┘└───────────────┘      └┘      
typ      └──┘└───────────────┘└┘ └┘└┘└┘└┘└┘
doc      └──┘                       └┘      
txt      └──┘                       └┘      
par      └──┘                       └┘      
pid        └┘                       └┘      
st   ─────────────────────────────────┘└────────┘└──
237      congr, funext n, rw outer_measure'_eq m m0 @mU
id                           └───────────────┘  └┘  └┘
src      └───┘  └──────┘  └─┘└───────────────┘      
typ      └───┘  └──────┘  └─┘└───────────────┘└┘ └┘
doc             └──────┘  └─┘                       
txt      └───┘  └──────┘  └─┘                       
par      └───┘  └──────┘  └─┘                       
pid                   └┘                           
st   ────────┘└────────┘└───────────────────────────────
238    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
239    trimmed :=
240    show (outer_measure' m m0).trim = outer_measure' m m0, begin
id           └────────────┘  └┘ └──┘   └────────────┘  └┘
src          └────────────┘      └──┘   └────────────┘
typ          └────────────┘  └┘ └──┘   └────────────┘  └┘
doc          └────────────┘              └────────────┘
st                                                            └─────
241      unfold outer_measure.trim,
src      └───────────────────────┘
typ      └───────────────────────┘
doc      └───────────────────────┘
txt      └───────────────────────┘
par      └───────────────────────┘
pid            └─────────────────┘
st   ────────────────────────────┘└─
242      congr, funext s hs,
src      └───┘  └─────────┘
typ      └───┘  └─────────┘
doc             └─────────┘
txt      └───┘  └─────────┘
par      └───┘  └─────────┘
pid                   └───┘
st   ────────┘└───────────┘└─
243      exact outer_measure'_eq m m0 @mU hs
id             └───────────────┘  └┘  └┘ └┘
src      └────┘└───────────────┘        
typ      └────┘└───────────────┘└┘ └┘└┘
doc      └────┘                         
txt      └────┘                         
par      └────┘                         
pid                                    
st   ────────────────────────────────────────
244    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
245    ..outer_measure' m m0 }
id       └────────────┘  └┘
src      └────────────┘
typ      └────────────┘  └┘
doc      └────────────┘
246  
247  lemma of_measurable_apply {α} [measurable_space α]
id                                  └──────────────┘ 
src                                 └──────────────┘
typ                                 └──────────────┘ 
248    {m : Π (s : set α), is_measurable s → ennreal}
id                 └─┘    └───────────┘    └─────┘
src                └─┘     └───────────┘     └─────┘
typ                └─┘    └───────────┘    └─────┘
doc                        └───────────┘     └─────┘
249    {m0 : m ∅ is_measurable.empty = 0}
id             └─────────────────┘ 
src             └─────────────────┘ 
typ            └─────────────────┘ 
250    {mU : ∀ {f : ℕ → set α} (h : ∀i, is_measurable (f i)),
id                    └─┘           └───────────┘   
src                    └─┘             └───────────┘
typ                   └─┘           └───────────┘   
doc                                     └───────────┘
251      pairwise (disjoint on f) →
id       └──────┘  └──────┘ └┘ 
src      └──────┘  └──────┘ └┘
typ      └──────┘  └──────┘ └┘ 
doc      └──────┘  └──────┘
252      m (⋃i, f i) (is_measurable.Union h) = (∑i, m (f i) (h i))}
id              └─────────────────┘             
src                 └─────────────────┘       
typ             └─────────────────┘             
doc                                            
253    (s : set α) (hs : is_measurable s) :
id          └─┘         └───────────┘ 
src         └─┘          └───────────┘
typ         └─┘         └───────────┘ 
doc                      └───────────┘
254    of_measurable m m0 @mU s = m s hs :=
id     └───────────┘  └┘  └┘     └┘
src    └───────────┘            
typ    └───────────┘  └┘  └┘     └┘
255  outer_measure'_eq m m0 @mU hs
id   └───────────────┘  └┘  └┘ └┘
src  └───────────────┘
typ  └───────────────┘  └┘  └┘ └┘
256  
257  @[ext] lemma ext {α} [measurable_space α] :
id                         └──────────────┘ 
src                        └──────────────┘
typ                        └──────────────┘ 
doc    └─┘
258    ∀ {μ₁ μ₂ : measure α}, (∀s, is_measurable s → μ₁ s = μ₂ s) → μ₁ = μ₂
id               └─────┘        └───────────┘    └┘   └┘     └┘  └┘
src               └─────┘          └───────────┘                      
typ              └─────┘        └───────────┘    └┘   └┘     └┘  └┘
doc                                └───────────┘
259  | ⟨m₁, u₁, h₁⟩ ⟨m₂, u₂, h₂⟩ h := by congr; rw [← h₁, ← h₂];
id                                                    └┘    └┘
src                                      └───┘  └────┘  └──┘  
typ                                      └───┘  └────┘└┘└──┘└┘
doc                                             └────┘  └──┘  
txt                                      └───┘  └────┘  └──┘  
par                                      └───┘  └────┘  └──┘  
pid                                               └──┘  └──┘  
st                                      └──────────┘└──┘└────┘└─
260    exact outer_measure.trim_congr h
id           └──────────────────────┘ 
src    └────┘└──────────────────────┘ 
typ    └────┘└──────────────────────┘
doc    └────┘                         
txt    └────┘                         
par    └────┘                         
pid                                  
st   ───────────────────────────────────
261  
src  
typ  
doc  
txt  
par  
pid  
st   
262  end measure
263  
264  section
265  variables {α : Type*} {β : Type*} [measurable_space α] {μ μ₁ μ₂ : measure α} {s s₁ s₂ : set α}
id                                     └──────────────┘               └─────┘               └─┘
src                                     └──────────────┘               └─────┘               └─┘
typ                                    └──────────────┘               └─────┘               └─┘
266  
267  @[simp] lemma to_outer_measure_apply (s) : μ.to_outer_measure s = μ s := rfl
id                                              └───────────────┘        └─┘
src                                              └───────────────┘           └─┘
typ                                             └───────────────┘        └─┘
doc    └──┘
268  
269  lemma measure_eq_trim (s) : μ s = μ.to_outer_measure.trim s :=
id                                  └───────────────┘└───┘ 
src                                    └───────────────┘└───┘
typ                                 └───────────────┘└───┘ 
270  by rw μ.trimmed; refl
src     └─┘           └────
typ     └─┘└───────┘  └────
doc     └─┘           └────
txt     └─┘           └────
par     └─┘           └────
pid                      
st     └───────────────────
271  
src  
typ  
doc  
txt  
par  
pid  
st   
272  lemma measure_eq_infi (s) : μ s = ⨅ t (st : s ⊆ t) (ht : is_measurable t), μ t :=
id                                                    └───────────┘    
src                                                        └───────────┘   
typ                                                   └───────────┘    
doc                                                          └───────────┘   
273  by rw [measure_eq_trim, outer_measure.trim_eq_infi]; refl
id          └─────────────┘  └────────────────────────┘
src     └──┘└─────────────┘└┘└────────────────────────┘  └────
typ     └──┘└─────────────┘└┘└────────────────────────┘  └────
doc     └──┘               └┘                            └────
txt     └──┘               └┘                            └────
par     └──┘               └┘                            └────
pid       └┘               └┘                                
st     └──────────────────┘└──────────────────────────┘└──────
274  
src  
typ  
doc  
txt  
par  
pid  
st   
275  lemma measure_eq_outer_measure' :
276    μ s = outer_measure' (λ s _, μ s) μ.empty s :=
id        └────────────┘          └────┘ 
src         └────────────┘               └────┘
typ       └────────────┘          └────┘ 
doc          └────────────┘
277  measure_eq_trim _
id   └─────────────┘
src  └─────────────┘
typ  └─────────────┘
278  
279  lemma to_outer_measure_eq_outer_measure' :
280    μ.to_outer_measure = outer_measure' (λ s _, μ s) μ.empty :=
id     └───────────────┘  └────────────┘          └────┘
src     └───────────────┘  └────────────┘               └────┘
typ    └───────────────┘  └────────────┘          └────┘
doc                         └────────────┘
281  μ.trimmed.symm
id   └──────┘└───┘
src   └──────┘└───┘
typ  └──────┘└───┘
282  
283  lemma measure_eq_measure' (hs : is_measurable s) :
id                                   └───────────┘ 
src                                  └───────────┘
typ                                  └───────────┘ 
doc                                  └───────────┘
284    μ s = measure' (λ s _, μ s) μ.empty s :=
id        └──────┘          └────┘ 
src         └──────┘               └────┘
typ       └──────┘          └────┘ 
doc          └──────┘
285  by rw [measure_eq_outer_measure',
id          └───────────────────────┘
src     └──┘└───────────────────────┘└─
typ     └──┘└───────────────────────┘└─
doc     └──┘                         └─
txt     └──┘                         └─
par     └──┘                         └─
pid       └┘                         └─
st     └────────────────────────────┘└─
286    outer_measure'_eq_measure' (λ s _, μ s) _ μ.m_Union hs]
id     └────────────────────────┘                └───────┘ └┘
src  ─┘└────────────────────────┘  └────┘  └──┘└───────┘  └─
typ  ─┘└────────────────────────┘  └────┘  └──┘└───────┘└┘└─
doc  ─┘                            └────┘  └──┘           └─
txt  ─┘                            └────┘  └──┘           └─
par  ─┘                            └────┘  └──┘           └─
pid  ─┘                            └────┘  └──┘           
st   ───────────────────────────────────────────────────────┘
287  
src  
typ  
doc  
txt  
par  
pid  
st   
288  @[simp] lemma measure_empty : μ ∅ = 0 := μ.empty
id                                         └────┘
src                                          └────┘
typ                                        └────┘
doc    └──┘
289  
290  lemma measure_mono (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂ := μ.mono h
id                           └┘  └┘     └┘   └┘    └───┘ 
src                                                   └───┘
typ                          └┘  └┘     └┘   └┘    └───┘ 
291  
292  lemma measure_mono_null (h : s₁ ⊆ s₂) (h₂ : μ s₂ = 0) : μ s₁ = 0 :=
id                                └┘  └┘         └┘        └┘ 
src                                                             
typ                               └┘  └┘         └┘        └┘ 
293  by rw [← le_zero_iff_eq, ← h₂]; exact measure_mono h
id            └────────────┘    └┘         └──────────┘ 
src     └────┘└────────────┘└──┘    └────┘└──────────┘ 
typ     └────┘└────────────┘└──┘└┘  └────┘└──────────┘
doc     └────┘              └──┘    └────┘             
txt     └────┘              └──┘    └────┘             
par     └────┘              └──┘    └────┘             
pid       └──┘              └──┘                      
st     └───────────────────┘└────┘└──────────────────────
294  
src  
typ  
doc  
txt  
par  
pid  
st   
295  lemma exists_is_measurable_superset_of_measure_eq_zero {s : set α} (h : μ s = 0) :
id                                                               └─┘          
src                                                              └─┘             
typ                                                              └─┘          
296    ∃t, s ⊆ t ∧ is_measurable t ∧ μ t = 0 :=
id          └───────────┘     
src            └───────────┘        
typ         └───────────┘     
doc                └───────────┘
297  begin
st   └─────
298    rw [measure_eq_infi] at h,
id         └─────────────┘
src    └──┘└─────────────┘└────┘
typ    └──┘└─────────────┘└────┘
doc    └──┘               └────┘
txt    └──┘               └────┘
par    └──┘               └────┘
pid      └┘               └───┘
st   ────────────────────┘└───┘└─
299    have h := (infi_eq_bot _).1 h,
id                └─────────┘      
src    └────────┘ └─────────┘└────┘
typ    └────────┘ └─────────┘└────┘
doc    └────────┘            └────┘
txt    └────────┘            └────┘
par    └────────┘            └────┘
pid    └────┘└─┘            └────┘
st   ──────────────────────────────┘└─
300    choose t ht using show ∀n:ℕ, ∃t, s ⊆ t ∧ is_measurable t ∧ μ t < n⁻¹,
id                                          └───────────┘          └┘
src    └────────────────┘     └┘     └───────────┘     └┘└─
typ    └────────────────┘     └┘    └───────────┘    └┘└─
doc    └────────────────┘     └┘        └───────────┘        └─
txt    └────────────────┘     └┘                             └─
par    └────────────────┘     └┘                             └─
pid          └┘└─┘└─────┘     └┘                             └─
st   ────────────────────────────────────────────────────────────────────────
301    { assume n,
src  ───┘└──────┘└─
typ  ───┘└──────┘└─
doc  ───┘└──────┘└─
txt  ───┘└──────┘└─
par  ───┘└──────┘└─
pid  ──────────────
st   ──┘└───────┘└─
302      have : (0 : ennreal) < n⁻¹ :=
id                   └─────┘    
src  ───┘└─────┘ └──┘└─────┘└┘    └───
typ  ───┘└─────┘ └──┘└─────┘└┘   └───
doc  ───┘└─────┘ └──┘└─────┘└┘    └───
txt  ───┘└─────┘ └──┘       └┘    └───
par  ───┘└─────┘ └──┘       └┘    └───
pid  ──────────┘ └──┘       └┘    └───
st   ──────────────────────────────────
303        (zero_lt_iff_ne_zero.2 $ ennreal.inv_ne_zero.2 $ ennreal.nat_ne_top _),
id          └─────────────────┘     └─────────────────┘     └────────────────┘
src  ─────┘ └─────────────────┘└─┘ └─────────────────┘└─┘ └────────────────┘└─┘└─
typ  ─────┘ └─────────────────┘└─┘ └─────────────────┘└─┘ └────────────────┘└─┘└─
doc  ─────┘                    └─┘                    └─┘                   └─┘└─
txt  ─────┘                    └─┘                    └─┘                   └─┘└─
par  ─────┘                    └─┘                    └─┘                   └─┘└─
pid  ─────┘                    └─┘                    └─┘                   └────
st   ───────────────────────────────────────────────────────────────────────────┘└─
304      rcases h _ this with ⟨t, ht⟩,
id                 └──┘
src  ───┘└─────┘ └─┘    └───────────┘└─
typ  ───┘└─────┘└─┘└──┘└───────────┘└─
doc  ───┘└─────┘ └─┘    └───────────┘└─
txt  ───┘└─────┘ └─┘    └───────────┘└─
par  ───┘└─────┘ └─┘    └───────────┘└─
pid  ──────────┘ └─┘    └──────────────
st   ───────────────────────────────┘└─
305      use [t],
id            
src  ───┘└───┘ └─
typ  ───┘└───┘└─
doc  ───┘└───┘ └─
txt  ───┘└───┘ └─
par  ───┘└───┘ └─
pid  ────────┘ └──
st   ──────────┘└─
306      simpa [(>), infi_lt_iff, -add_comm] using ht },
id                  └─────────┘                   └┘
src  ───┘└─────┘└──┘└─────────┘└─────────────────┘  
typ  ───┘└─────┘└──┘└─────────┘└─────────────────┘└┘
doc  ───┘└─────┘ └──┘           └─────────────────┘  
txt  ───┘└─────┘ └──┘           └─────────────────┘  
par  ───┘└─────┘ └──┘           └─────────────────┘  
pid  ──────────┘ └──┘           └─────────────────┘  └┘
st   ────────────────────────────────────────────────┘└┘
307    refine ⟨⋂n, t n, subset_Inter (λn, (ht n).1), is_measurable.Inter (λn, (ht n).2.1), _⟩,
id                   └──────────┘                 └─────────────────┘       └┘
src    └─────┘   └┘└──────────┘  └─┘    └────┘└─────────────────┘  └─┘    └────────┘
typ    └─────┘  └┘└──────────┘  └─┘    └────┘└─────────────────┘  └─┘ └┘ └────────┘
doc    └─────┘   └┘              └─┘    └────┘                     └─┘    └────────┘
txt    └─────┘     └┘              └─┘    └────┘                     └─┘    └────────┘
par    └─────┘     └┘              └─┘    └────┘                     └─┘    └────────┘
pid               └┘              └─┘    └────┘                     └─┘    └────────┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
308    refine eq_of_le_of_forall_le_of_dense bot_le (assume r hr, _),
id            └────────────────────────────┘ └────┘
src    └─────┘└────────────────────────────┘└────┘       └───────┘
typ    └─────┘└────────────────────────────┘└────┘       └───────┘
doc    └─────┘                                           └───────┘
txt    └─────┘                                           └───────┘
par    └─────┘                                           └───────┘
pid                                                     └───────┘
st   ──────────────────────────────────────────────────────────────┘└─
309    rcases ennreal.exists_inv_nat_lt (ne_of_gt hr) with ⟨n, hn⟩,
id            └───────────────────────┘  └──────┘ └┘
src    └─────┘└───────────────────────┘ └──────┘  └────────────┘
typ    └─────┘└───────────────────────┘ └──────┘└┘└────────────┘
doc    └─────┘                                    └────────────┘
txt    └─────┘                                    └────────────┘
par    └─────┘                                    └────────────┘
pid                                              └────────────┘
st   ────────────────────────────────────────────────────────────┘└─
310    calc μ (⋂n, t n) ≤ μ (t n) : measure_mono (Inter_subset _ _)
id     └──┘                      └──────────┘  └──────────┘
src    └──┘                         └──────────┘  └──────────┘
typ    └──┘                      └──────────┘  └──────────┘
doc    └──┘
st   ───────────────────────────────────────────────────────────────
311      ... ≤ n⁻¹ : le_of_lt (ht n).2.2
id                             └┘   
src                                  
typ                            └┘   
st   ────────────────────────────────────
312      ... ≤ r : le_of_lt hn
id                └──────┘ └┘
src                └──────┘
typ               └──────┘ └┘
st   ────────────────────────┘
313  end
st   ──┘
314  
315  theorem measure_Union_le {β} [encodable β] (s : β → set α) : μ (⋃i, s i) ≤ (∑i, μ (s i)) :=
id                                 └───────┘           └─┘                 
src                                └───────┘             └─┘                   
typ                                └───────┘           └─┘                 
doc                                └───────┘                                    
316  μ.to_outer_measure.Union _
id   └───────────────┘└────┘
src   └───────────────┘└────┘
typ  └───────────────┘└────┘
317  
318  lemma measure_Union_null {β} [encodable β] {s : β → set α} :
id                                 └───────┘           └─┘ 
src                                └───────┘             └─┘
typ                                └───────┘           └─┘ 
doc                                └───────┘
319    (∀ i, μ (s i) = 0) → μ (⋃i, s i) = 0 :=
id                           
src                                  
typ                          
doc                             
320  μ.to_outer_measure.Union_null
id   └───────────────┘└─────────┘
src   └───────────────┘└─────────┘
typ  └───────────────┘└─────────┘
321  
322  theorem measure_union_le (s₁ s₂ : set α) : μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂ :=
id                                     └─┘       └┘  └┘    └┘   └┘
src                                    └─┘                       
typ                                    └─┘       └┘  └┘    └┘   └┘
323  μ.to_outer_measure.union _ _
id   └───────────────┘└────┘
src   └───────────────┘└────┘
typ  └───────────────┘└────┘
324  
325  lemma measure_union_null {s₁ s₂ : set α} : μ s₁ = 0 → μ s₂ = 0 → μ (s₁ ∪ s₂) = 0 :=
id                                     └─┘      └┘       └┘        └┘  └┘  
src                                    └─┘                                     
typ                                    └─┘      └┘       └┘        └┘  └┘  
326  μ.to_outer_measure.union_null
id   └───────────────┘└─────────┘
src   └───────────────┘└─────────┘
typ  └───────────────┘└─────────┘
327  
328  lemma measure_Union {β} [encodable β] {f : β → set α}
id                            └───────┘           └─┘ 
src                           └───────┘             └─┘
typ                           └───────┘           └─┘ 
doc                           └───────┘
329    (hn : pairwise (disjoint on f)) (h : ∀i, is_measurable (f i)) :
id           └──────┘  └──────┘ └┘            └───────────┘   
src          └──────┘  └──────┘ └┘              └───────────┘
typ          └──────┘  └──────┘ └┘            └───────────┘   
doc          └──────┘  └──────┘                 └───────────┘
330    μ (⋃i, f i) = (∑i, μ (f i)) :=
id                 
src                 
typ                
doc                  
331  by rw [measure_eq_measure' (is_measurable.Union h),
id          └─────────────────┘  └─────────────────┘ 
src     └──┘└─────────────────┘ └─────────────────┘ └──
typ     └──┘└─────────────────┘ └─────────────────┘└──
doc     └──┘                                        └──
txt     └──┘                                        └──
par     └──┘                                        └──
pid       └┘                                        └──
st     └──────────────────────────────────────────────┘└─
332       measure'_Union (λ s _, μ s) _ μ.m_Union hn h];
id        └────────────┘                └───────┘ └┘ 
src  ────┘└────────────┘  └────┘  └──┘└───────┘   
typ  ────┘└────────────┘  └────┘  └──┘└───────┘└┘
doc  ────┘                └────┘  └──┘            
txt  ────┘                └────┘  └──┘            
par  ────┘                └────┘  └──┘            
pid  ────┘                └────┘  └──┘            
st   ────────────────────────────────────────────────┘└─
333     simp [measure_eq_measure', h]
id            └─────────────────┘  
src     └────┘└─────────────────┘└┘ └─
typ     └────┘└─────────────────┘└┘└─
doc     └────┘                   └┘ └─
txt     └────┘                   └┘ └─
par     └────┘                   └┘ └─
pid                            └┘ 
st   ─────────────────────────────────
334  
src  
typ  
doc  
txt  
par  
pid  
st   
335  lemma measure_union (hd : disjoint s₁ s₂) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
id                             └──────┘ └┘ └┘        └───────────┘ └┘        └───────────┘ └┘
src                            └──────┘              └───────────┘           └───────────┘
typ                            └──────┘ └┘ └┘        └───────────┘ └┘        └───────────┘ └┘
doc                            └──────┘              └───────────┘           └───────────┘
336    μ (s₁ ∪ s₂) = μ s₁ + μ s₂ :=
id       └┘  └┘    └┘   └┘
src                     
typ      └┘  └┘    └┘   └┘
337  by rw [measure_eq_measure' (h₁.union h₂),
id          └─────────────────┘  └──────┘ └┘
src     └──┘└─────────────────┘ └──────┘  └──
typ     └──┘└─────────────────┘ └──────┘└┘└──
doc     └──┘                              └──
txt     └──┘                              └──
par     └──┘                              └──
pid       └┘                              └──
st     └────────────────────────────────────┘└─
338       measure'_union (λ s _, μ s) _ μ.m_Union hd h₁ h₂];
id        └────────────┘                └───────┘ └┘ └┘ └┘
src  ────┘└────────────┘  └────┘  └──┘└───────┘      
typ  ────┘└────────────┘  └────┘  └──┘└───────┘└┘└┘└┘
doc  ────┘                └────┘  └──┘               
txt  ────┘                └────┘  └──┘               
par  ────┘                └────┘  └──┘               
pid  ────┘                └────┘  └──┘               
st   ────────────────────────────────────────────────────┘└─
339     simp [measure_eq_measure', h₁, h₂]
id            └─────────────────┘  └┘  └┘
src     └────┘└─────────────────┘└┘  └┘  └─
typ     └────┘└─────────────────┘└┘└┘└┘└┘└─
doc     └────┘                   └┘  └┘  └─
txt     └────┘                   └┘  └┘  └─
par     └────┘                   └┘  └┘  └─
pid                            └┘  └┘  
st   ──────────────────────────────────────
340  
src  
typ  
doc  
txt  
par  
pid  
st   
341  lemma measure_bUnion {s : set β} {f : β → set α} (hs : countable s)
id                             └─┘           └─┘         └───────┘ 
src                            └─┘             └─┘          └───────┘
typ                            └─┘           └─┘         └───────┘ 
doc                                                         └───────┘
342    (hd : pairwise_on s (disjoint on f)) (h : ∀b∈s, is_measurable (f b)) :
id           └─────────┘   └──────┘ └┘             └───────────┘   
src          └─────────┘    └──────┘ └┘               └───────────┘
typ          └─────────┘   └──────┘ └┘             └───────────┘   
doc          └─────────┘    └──────┘                   └───────────┘
343    μ (⋃b∈s, f b) = ∑p:s, μ (f p.1) :=
id                   
src                           
typ                  
doc                     
344  begin
st   └─────
345    haveI := hs.to_encodable,
id              └─────────────┘
src    └───────┘└─────────────┘
typ    └───────┘└─────────────┘
doc    └───────┘
txt    └───────┘
par    └───────┘
pid         └─┘
st   ─────────────────────────┘└─
346    rw [← measure_Union, bUnion_eq_Union],
id           └───────────┘  └─────────────┘
src    └────┘└───────────┘└┘└─────────────┘
typ    └────┘└───────────┘└┘└─────────────┘
doc    └────┘             └┘               
txt    └────┘             └┘               
par    └────┘             └┘               
pid      └──┘             └┘               
st   ────────────────────┘└───────────────┘└──
347    { rintro ⟨i, hi⟩ ⟨j, hj⟩ ij x ⟨h₁, h₂⟩,
src      └──────────────────────────────────┘
typ      └──────────────────────────────────┘
doc      └──────────────────────────────────┘
txt      └──────────────────────────────────┘
par      └──────────────────────────────────┘
pid            └────────────────────────────┘
st   ───┘└──────────────────────────────────┘└─
348      exact hd i hi j hj (mt subtype.eq' ij:_) ⟨h₁, h₂⟩ },
id             └┘  └┘  └┘  └┘ └─────────┘ └┘     └┘  └┘
src      └────┘         └┘└─────────┘  └──┘   └┘  └┘
typ      └────┘└┘└┘└┘ └┘└─────────┘└┘└──┘ └┘└┘└┘└┘
doc      └────┘                        └──┘   └┘  └┘
txt      └────┘                        └──┘   └┘  └┘
par      └────┘                        └──┘   └┘  └┘
pid                                   └──┘   └┘  
st   ─────────────────────────────────────────────────────┘└┘
349    { simpa }
src      └────┘
typ      └────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ─────────┘└─
350  end
st   ──┘
351  
352  lemma measure_sUnion {S : set (set α)} (hs : countable S)
id                             └─┘  └─┘          └───────┘ 
src                            └─┘  └─┘           └───────┘
typ                            └─┘  └─┘          └───────┘ 
doc                                               └───────┘
353    (hd : pairwise_on S disjoint) (h : ∀s∈S, is_measurable s) :
id           └─────────┘  └──────┘           └───────────┘ 
src          └─────────┘   └──────┘             └───────────┘
typ          └─────────┘  └──────┘           └───────────┘ 
doc          └─────────┘   └──────┘             └───────────┘
354    μ (⋃₀ S) = ∑s:S, μ s.1 :=
id       └┘        
src       └┘            
typ      └┘        
doc                  
355  by rw [sUnion_eq_bUnion, measure_bUnion hs hd h]
id          └──────────────┘  └────────────┘ └┘ └┘ 
src     └──┘└──────────────┘└┘└────────────┘     └─
typ     └──┘└──────────────┘└┘└────────────┘└┘└┘└─
doc     └──┘                └┘                   └─
txt     └──┘                └┘                   └─
par     └──┘                └┘                   └─
pid       └┘                └┘                   
st     └───────────────────┘└──────────────────────┘
356  
src  
typ  
doc  
txt  
par  
pid  
st   
357  lemma measure_diff {s₁ s₂ : set α} (h : s₂ ⊆ s₁)
id                               └─┘        └┘  └┘
src                              └─┘            
typ                              └─┘        └┘  └┘
358    (h₁ : is_measurable s₁) (h₂ : is_measurable s₂)
id           └───────────┘ └┘        └───────────┘ └┘
src          └───────────┘           └───────────┘
typ          └───────────┘ └┘        └───────────┘ └┘
doc          └───────────┘           └───────────┘
359    (h_fin : μ s₂ < ⊤) : μ (s₁ \ s₂) = μ s₁ - μ s₂ :=
id               └┘        └┘  └┘    └┘   └┘
src                                        
typ              └┘        └┘  └┘    └┘   └┘
360  begin
st   └─────
361    refine (ennreal.add_sub_self' h_fin).symm.trans _,
id             └───────────────────┘ └───┘
src    └─────┘ └───────────────────┘     └────────────┘
typ    └─────┘ └───────────────────┘└───┘└────────────┘
doc    └─────┘                           └────────────┘
txt    └─────┘                           └────────────┘
par    └─────┘                           └────────────┘
pid                                     └────────────┘
st   ──────────────────────────────────────────────────┘└─
362    rw [← measure_union disjoint_diff h₂ (h₁.diff h₂), union_diff_cancel h]
id           └───────────┘ └───────────┘     └─────┘ └┘   └───────────────┘ 
src    └────┘└───────────┘└───────────┘   └─────┘  └─┘└───────────────┘ └┘
typ    └────┘└───────────┘└───────────┘   └─────┘└┘└─┘└───────────────┘└┘
doc    └────┘                                      └─┘                  └┘
txt    └────┘                                      └─┘                  └┘
par    └────┘                                      └─┘                  └┘
pid      └──┘                                      └─┘                  
st   ──────────────────────────────────────────────────┘└───────────────────┘
363  end
st   └─┘
364  
365  lemma measure_Union_eq_supr_nat {s : ℕ → set α} (h : ∀i, is_measurable (s i)) (hs : monotone s) :
id                                           └─┘           └───────────┘            └──────┘ 
src                                          └─┘             └───────────┘              └──────┘
typ                                          └─┘           └───────────┘            └──────┘ 
doc                                                           └───────────┘              └──────┘
366    μ (⋃i, s i) = (⨆i, μ (s i)) :=
id                 
src                 
typ                
doc                  
367  begin
st   └─────
368    refine le_antisymm _ (supr_le $ λ i, measure_mono $ subset_Union _ _),
id            └─────────┘    └─────┘        └──────────┘   └──────────┘
src    └─────┘└─────────┘└─┘ └─────┘  └──┘└──────────┘ └──────────┘└───┘
typ    └─────┘└─────────┘└─┘ └─────┘  └──┘└──────────┘ └──────────┘└───┘
doc    └─────┘           └─┘          └──┘                         └───┘
txt    └─────┘           └─┘          └──┘                         └───┘
par    └─────┘           └─┘          └──┘                         └───┘
pid                     └─┘          └──┘                         └───┘
st   ──────────────────────────────────────────────────────────────────────┘└─
369    rw [← Union_disjointed,
id           └──────────────┘
src    └────┘└──────────────┘└─
typ    └────┘└──────────────┘└─
doc    └────┘                └─
txt    └────┘                └─
par    └────┘                └─
pid      └──┘                └─
st   ───────────────────────┘└─
370      measure_Union disjoint_disjointed (is_measurable.disjointed h),
id       └───────────┘ └─────────────────┘  └──────────────────────┘ 
src  ───┘└───────────┘└─────────────────┘ └──────────────────────┘ └──
typ  ───┘└───────────┘└─────────────────┘ └──────────────────────┘└──
doc  ───┘                                                          └──
txt  ───┘                                                          └──
par  ───┘                                                          └──
pid  ───┘                                                          └──
st   ─────────────────────────────────────────────────────────────────┘└─
371      ennreal.tsum_eq_supr_nat],
id       └──────────────────────┘
src  ───┘└──────────────────────┘
typ  ───┘└──────────────────────┘
doc  ───┘                        
txt  ───┘                        
par  ───┘                        
pid  ───┘                        
st   ───────────────────────────┘└──
372    refine supr_le (λ n, _),
id            └─────┘
src    └─────┘└─────┘  └────┘
typ    └─────┘└─────┘  └────┘
doc    └─────┘         └────┘
txt    └─────┘         └────┘
par    └─────┘         └────┘
pid                   └────┘
st   ────────────────────────┘└─
373    cases n, {apply zero_le _},
id                    └─────┘
src    └────┘    └────┘└─────┘└┘
typ    └────┘   └────┘└─────┘└┘
doc    └────┘    └────┘       └┘
txt    └────┘    └────┘       └┘
par    └────┘    └────┘       └┘
pid                         └┘
st   ────────┘└────────────────┘└┘
374    suffices : sum (finset.range n.succ) (λ i, μ (disjointed s i)) = μ (s n),
id                └─┘  └──────────┘ └────┘           └────────┘           
src    └─────────┘└─┘ └──────────┘└────┘└┘  └──┘  └────────┘  └─┘    
typ    └─────────┘└─┘ └──────────┘└────┘└┘  └──┘  └────────┘  └─┘ 
doc    └─────────┘    └──────────┘      └┘  └──┘  └────────┘  └─┘     
txt    └─────────┘                      └┘  └──┘              └─┘     
par    └─────────┘                      └┘  └──┘              └─┘     
pid    └───────┘└┘                      └┘  └──┘              └─┘     
st   ─────────────────────────────────────────────────────────────────────────┘└─
375    { rw this, exact le_supr _ n },
id          └──┘        └─────┘   
src      └─┘      └────┘└─────┘└─┘ 
typ      └─┘└──┘  └────┘└─────┘└─┘
doc      └─┘      └────┘       └─┘ 
txt      └─┘      └────┘       └─┘ 
par      └─┘      └────┘       └─┘ 
pid                          └─┘ 
st   ───┘└─────┘└──────────────────┘└┘
376    rw [← Union_disjointed_of_mono hs, measure_Union, tsum_eq_sum],
id           └──────────────────────┘ └┘  └───────────┘  └─────────┘
src    └────┘└──────────────────────┘  └┘└───────────┘└┘└─────────┘
typ    └────┘└──────────────────────┘└┘└┘└───────────┘└┘└─────────┘
doc    └────┘                          └┘             └┘           
txt    └────┘                          └┘             └┘           
par    └────┘                          └┘             └┘           
pid      └──┘                          └┘             └┘           
st   ──────────────────────────────────┘└─────────────┘└───────────┘└──
377    { apply sum_congr rfl, intros i hi,
id             └───────┘ └─┘
src      └────┘└───────┘└─┘  └─────────┘
typ      └────┘└───────┘└─┘  └─────────┘
doc      └────┘              └─────────┘
txt      └────┘              └─────────┘
par      └────┘              └─────────┘
pid                               └───┘
st   ───┘└─────────────────┘└───────────┘└─
378      simp [finset.mem_range.1 hi] },
id             └──────────────┘   └┘
src      └────┘└──────────────┘└─┘  └┘
typ      └────┘└──────────────┘└─┘└┘└┘
doc      └────┘                └─┘  └┘
txt      └────┘                └─┘  └┘
par      └────┘                └─┘  └┘
pid                          └─┘  
st   ────────────────────────────────┘└┘
379    { intros i hi, simp [mt finset.mem_range.2 hi] },
id                          └┘ └──────────────┘   └┘
src      └─────────┘  └────┘└┘└──────────────┘└─┘  └┘
typ      └─────────┘  └────┘└┘└──────────────┘└─┘└┘└┘
doc      └─────────┘  └────┘                  └─┘  └┘
txt      └─────────┘  └────┘                  └─┘  └┘
par      └─────────┘  └────┘                  └─┘  └┘
pid            └───┘                        └─┘  
st   ───┘└─────────┘└────────────────────────────────┘└┘
380    { rintro i j ij x ⟨⟨_, ⟨_, rfl⟩, h₁⟩, ⟨_, ⟨_, rfl⟩, h₂⟩⟩,
src      └────────────────────────────────────────────────────┘
typ      └────────────────────────────────────────────────────┘
doc      └────────────────────────────────────────────────────┘
txt      └────────────────────────────────────────────────────┘
par      └────────────────────────────────────────────────────┘
pid            └──────────────────────────────────────────────┘
st   ───┘└────────────────────────────────────────────────────┘└─
381      exact disjoint_disjointed i j ij ⟨h₁, h₂⟩ },
id             └─────────────────┘   └┘  └┘  └┘
src      └────┘└─────────────────┘       └┘  └┘
typ      └────┘└─────────────────┘└┘ └┘└┘└┘└┘
doc      └────┘                          └┘  └┘
txt      └────┘                          └┘  └┘
par      └────┘                          └┘  └┘
pid                                     └┘  
st   ─────────────────────────────────────────────┘└┘
382    { intro i,
src      └─────┘
typ      └─────┘
doc      └─────┘
txt      └─────┘
par      └─────┘
pid           └┘
st   ──────────┘└─
383      by_cases h' : i < n.succ; simp [h', is_measurable.empty],
id                       └────┘        └┘  └─────────────────┘
src      └───────┘  └─┘ └────┘  └────┘  └┘└─────────────────┘
typ      └───────┘  └─┘└────┘  └────┘└┘└┘└─────────────────┘
doc      └───────┘  └─┘          └────┘  └┘                   
txt      └───────┘  └─┘          └────┘  └┘                   
par      └───────┘  └─┘          └────┘  └┘                   
pid                └─┘                └┘                   
st   ───────────────────────────────────────────────────────────┘└─
384      apply is_measurable.disjointed h }
id             └──────────────────────┘ 
src      └────┘└──────────────────────┘ 
typ      └────┘└──────────────────────┘
doc      └────┘                         
txt      └────┘                         
par      └────┘                         
pid                                    
st   ────────────────────────────────────┘└─
385  end
st   ──┘
386  
387  lemma measure_Inter_eq_infi_nat {s : ℕ → set α}
id                                           └─┘ 
src                                          └─┘
typ                                          └─┘ 
388    (h : ∀i, is_measurable (s i)) (hs : ∀i j, i ≤ j → s j ⊆ s i)
id             └───────────┘                         
src             └───────────┘                               
typ            └───────────┘                         
doc             └───────────┘
389    (hfin : ∃i, μ (s i) < ⊤) :
id                    
src                       
typ                   
390    μ (⋂i, s i) = (⨅i, μ (s i)) :=
id                 
src                 
typ                
doc                  
391  begin
st   └─────
392    rcases hfin with ⟨k, hk⟩,
id            └──┘
src    └─────┘    └───────────┘
typ    └─────┘└──┘└───────────┘
doc    └─────┘    └───────────┘
txt    └─────┘    └───────────┘
par    └─────┘    └───────────┘
pid              └───────────┘
st   ─────────────────────────┘└─
393    rw [← ennreal.sub_sub_cancel (by exact hk) (infi_le _ k),
id           └────────────────────┘           └┘   └─────┘   
src    └────┘└────────────────────┘   └────┘  └┘ └─────┘└─┘ └──
typ    └────┘└────────────────────┘   └────┘└┘└┘ └─────┘└─┘└──
doc    └────┘                         └────┘  └┘        └─┘ └──
txt    └────┘                         └────┘  └┘        └─┘ └──
par    └────┘                         └────┘  └┘        └─┘ └──
pid      └──┘                         └─────┘  └┘        └─┘ └──
st   ─────────────────────────────────┘└───────┘└─────────────┘└─
394      ennreal.sub_infi,
id       └──────────────┘
src  ───┘└──────────────┘└─
typ  ───┘└──────────────┘└─
doc  ───┘                └─
txt  ───┘                └─
par  ───┘                └─
pid  ───┘                └─
st   ───────────────────┘└─
395      ← ennreal.sub_sub_cancel (by exact hk) (measure_mono (Inter_subset _ k)),
id         └────────────────────┘           └┘   └──────────┘  └──────────┘   
src  ─────┘└────────────────────┘   └────┘  └┘ └──────────┘ └──────────┘└─┘ └───
typ  ─────┘└────────────────────┘   └────┘└┘└┘ └──────────┘ └──────────┘└─┘└───
doc  ─────┘                         └────┘  └┘                          └─┘ └───
txt  ─────┘                         └────┘  └┘                          └─┘ └───
par  ─────┘                         └────┘  └┘                          └─┘ └───
pid  ─────┘                         └─────┘  └┘                          └─┘ └───
st   ───────────────────────────────┘└───────┘└─────────────────────────────────┘└─
396      ← measure_diff (Inter_subset _ k) (h k) (is_measurable.Inter h)
id         └──────────┘                           └─────────────────┘ 
src  ─────┘└──────────┘             └─┘ └┘   └┘ └─────────────────┘ └─
typ  ─────┘└──────────┘             └─┘ └┘   └┘ └─────────────────┘└─
doc  ─────┘                         └─┘ └┘   └┘                     └─
txt  ─────┘                         └─┘ └┘   └┘                     └─
par  ─────┘                         └─┘ └┘   └┘                     └─
pid  ─────┘                         └─┘ └┘   └┘                     └─
st   ────────────────────────────────────────────────────────────────────
397        (lt_of_le_of_lt (measure_mono (Inter_subset _ k)) hk),
id          └────────────┘  └──────────┘  └──────────┘      └┘
src  ─────┘ └────────────┘ └──────────┘ └──────────┘└─┘ └─┘  └──
typ  ─────┘ └────────────┘ └──────────┘ └──────────┘└─┘└─┘└┘└──
doc  ─────┘                                         └─┘ └─┘  └──
txt  ─────┘                                         └─┘ └─┘  └──
par  ─────┘                                         └─┘ └─┘  └──
pid  ─────┘                                         └─┘ └─┘  └──
st   ──────────────────────────────────────────────────────────┘└─
398      diff_Inter, measure_Union_eq_supr_nat],
id       └────────┘  └───────────────────────┘
src  ───┘└────────┘└┘└───────────────────────┘
typ  ───┘└────────┘└┘└───────────────────────┘
doc  ───┘          └┘                         
txt  ───┘          └┘                         
par  ───┘          └┘                         
pid  ───┘          └┘                         
st   ─────────────┘└─────────────────────────┘└──
399    { congr, funext i,
src      └───┘  └──────┘
typ      └───┘  └──────┘
doc             └──────┘
txt      └───┘  └──────┘
par      └───┘  └──────┘
pid                   └┘
st   ───┘└───┘└────────┘└─
400      cases le_total k i with ik ik,
id             └──────┘  
src      └────┘└──────┘  └─────────┘
typ      └────┘└──────┘└─────────┘
doc      └────┘          └─────────┘
txt      └────┘          └─────────┘
par      └────┘          └─────────┘
pid                     └─────────┘
st   ────────────────────────────────┘└─
401      { exact measure_diff (hs _ _ ik) (h k) (h i)
id               └──────────┘                    
src        └────┘└──────────┘   └───┘  └┘   └┘   └─
typ        └────┘└──────────┘   └───┘  └┘  └┘ └─
doc        └────┘               └───┘  └┘   └┘   └─
txt        └────┘               └───┘  └┘   └┘   └─
par        └────┘               └───┘  └┘   └┘   └─
pid                            └───┘  └┘   └┘   └─
st   ─────┘└──────────────────────────────────────────
402          (lt_of_le_of_lt (measure_mono (hs _ _ ik)) hk) },
id            └────────────┘  └──────────┘  └┘     └┘   └┘
src  ───────┘ └────────────┘ └──────────┘   └───┘  └─┘  └┘
typ  ───────┘ └────────────┘ └──────────┘ └┘└───┘└┘└─┘└┘└┘
doc  ───────┘                               └───┘  └─┘  └┘
txt  ───────┘                               └───┘  └─┘  └┘
par  ───────┘                               └───┘  └─┘  └┘
pid  ───────┘                               └───┘  └─┘  
st   ──────────────────────────────────────────────────────┘└┘
403      { rw [diff_eq_empty.2 (hs _ _ ik), measure_empty,
id             └───────────┘    └┘     └┘   └───────────┘
src        └──┘└───────────┘└─┘   └───┘  └─┘└───────────┘└─
typ        └──┘└───────────┘└─┘ └┘└───┘└┘└─┘└───────────┘└─
doc        └──┘             └─┘   └───┘  └─┘             └─
txt        └──┘             └─┘   └───┘  └─┘             └─
par        └──┘             └─┘   └───┘  └─┘             └─
pid          └┘             └─┘   └───┘  └─┘             └─
st   ────────────────────────────────────┘└─────────────┘└─
404        ennreal.sub_eq_zero_of_le (measure_mono (hs _ _ ik))] } },
id         └───────────────────────┘  └──────────┘  └┘     └┘
src  ─────┘└───────────────────────┘ └──────────┘   └───┘  └──┘
typ  ─────┘└───────────────────────┘ └──────────┘ └┘└───┘└┘└──┘
doc  ─────┘                                         └───┘  └──┘
txt  ─────┘                                         └───┘  └──┘
par  ─────┘                                         └───┘  └──┘
pid  ─────┘                                         └───┘  └─┘
st   ─────────────────────────────────────────────────────────┘└──┘
405    { exact λ i, (h k).diff (h i) },
id                             
src      └────┘ └──┘   └─────┘   └┘
typ      └────┘ └──┘  └─────┘  └┘
doc      └────┘ └──┘   └─────┘   └┘
txt      └────┘ └──┘   └─────┘   └┘
par      └────┘ └──┘   └─────┘   └┘
pid            └──┘   └─────┘   
st   ───┘└──────────────────────────┘└┘
406    { exact λ i j ij, diff_subset_diff_right (hs _ _ ij) }
id                       └────────────────────┘  └┘
src      └────┘ └───────┘└────────────────────┘   └───┘  └┘
typ      └────┘ └───────┘└────────────────────┘ └┘└───┘  └┘
doc      └────┘ └───────┘                         └───┘  └┘
txt      └────┘ └───────┘                         └───┘  └┘
par      └────┘ └───────┘                         └───┘  └┘
pid            └───────┘                         └───┘  
st   ──────────────────────────────────────────────────────┘└─
407  end
st   ──┘
408  
409  lemma measure_eq_inter_diff {μ : measure α} {s t : set α}
id                                    └─────┘          └─┘ 
src                                   └─────┘           └─┘
typ                                   └─────┘          └─┘ 
410    (hs : is_measurable s) (ht : is_measurable t) :
id           └───────────┘         └───────────┘ 
src          └───────────┘          └───────────┘
typ          └───────────┘         └───────────┘ 
doc          └───────────┘          └───────────┘
411    μ s = μ (s ∩ t) + μ (s \ t) :=
id                   
src                        
typ                  
412  have hd : disjoint (s ∩ t) (s \ t) := assume a ⟨⟨_, hs⟩, _, hns⟩, hns hs ,
id             └──────┘                          └┘      └─┘
src            └──────┘           
typ            └──────┘                          └┘      └─┘
doc            └──────┘
413  by rw [← measure_union hd (hs.inter ht) (hs.diff ht), inter_union_diff s t]
id            └───────────┘ └┘  └──────┘      └─────┘ └┘   └──────────────┘  
src     └────┘└───────────┘   └──────┘  └┘ └─────┘  └─┘└──────────────┘  └─
typ     └────┘└───────────┘└┘ └──────┘  └┘ └─────┘└┘└─┘└──────────────┘└─
doc     └────┘                          └┘          └─┘                  └─
txt     └────┘                          └┘          └─┘                  └─
par     └────┘                          └┘          └─┘                  └─
pid       └──┘                          └┘          └─┘                  
st     └────────────────────────────────────────────────┘└────────────────────┘
414  
src  
typ  
doc  
txt  
par  
pid  
st   
415  lemma tendsto_measure_Union {μ : measure α} {s : ℕ → set α}
id                                    └─────┘           └─┘ 
src                                   └─────┘            └─┘
typ                                   └─────┘           └─┘ 
416    (hs : ∀n, is_measurable (s n)) (hm : monotone s) :
id              └───────────┘            └──────┘ 
src              └───────────┘              └──────┘
typ             └───────────┘            └──────┘ 
doc              └───────────┘              └──────┘
417    tendsto (μ ∘ s) at_top (𝓝 (μ (⋃n, s n))) :=
id     └─────┘      └────┘        
src    └─────┘        └────┘        
typ    └─────┘      └────┘        
doc    └─────┘         └────┘        
418  begin
st   └─────
419    rw measure_Union_eq_supr_nat hs hm,
id        └───────────────────────┘ └┘ └┘
src    └─┘└───────────────────────┘  
typ    └─┘└───────────────────────┘└┘└┘
doc    └─┘                           
txt    └─┘                           
par    └─┘                           
pid                                 
st   ───────────────────────────────────┘└─
420    exact tendsto_at_top_supr_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm $ hnm)
id           └─────────────────────┘                       └──────────┘   └┘
src    └────┘└─────────────────────┘   └┘       └────────┘└──────────┘       └┘
typ    └────┘└─────────────────────┘ └┘       └────────┘└──────────┘ └┘    └┘
doc    └────┘                           └┘       └────────┘                   └┘
txt    └────┘                           └┘       └────────┘                   └┘
par    └────┘                           └┘       └────────┘                   └┘
pid                                    └┘       └────────┘                   
st   ─────────────────────────────────────────────────────────────────────────────────┘
421  end
st   └─┘
422  
423  lemma tendsto_measure_Inter {μ : measure α} {s : ℕ → set α}
id                                    └─────┘           └─┘ 
src                                   └─────┘            └─┘
typ                                   └─────┘           └─┘ 
424    (hs : ∀n, is_measurable (s n)) (hm : ∀n m, n ≤ m → s m ⊆ s n) (hf : ∃i, μ (s i) < ⊤) :
id              └───────────┘                                        
src              └───────────┘                                                      
typ             └───────────┘                                        
doc              └───────────┘
425    tendsto (μ ∘ s) at_top (𝓝 (μ (⋂n, s n))) :=
id     └─────┘      └────┘        
src    └─────┘        └────┘        
typ    └─────┘      └────┘        
doc    └─────┘         └────┘        
426  begin
st   └─────
427    rw measure_Inter_eq_infi_nat hs hm hf,
id        └───────────────────────┘ └┘ └┘ └┘
src    └─┘└───────────────────────┘    
typ    └─┘└───────────────────────┘└┘└┘└┘
doc    └─┘                             
txt    └─┘                             
par    └─┘                             
pid                                   
st   ──────────────────────────────────────┘└─
428    exact tendsto_at_top_infi_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm _ _ $ hnm),
id           └─────────────────────┘                       └──────────┘   └┘
src    └────┘└─────────────────────┘   └┘       └────────┘└──────────┘   └───┘    
typ    └────┘└─────────────────────┘ └┘       └────────┘└──────────┘ └┘└───┘    
doc    └────┘                           └┘       └────────┘               └───┘    
txt    └────┘                           └┘       └────────┘               └───┘    
par    └────┘                           └┘       └────────┘               └───┘    
pid                                    └┘       └────────┘               └───┘    
st   ────────────────────────────────────────────────────────────────────────────────────┘└─
429  end
st   ──┘
430  
431  end
432  
433  def outer_measure.to_measure {α} (m : outer_measure α)
id                                         └───────────┘ 
src                                        └───────────┘
typ                                        └───────────┘ 
434    [ms : measurable_space α] (h : ms ≤ m.caratheodory) :
id           └──────────────┘        └┘  └───────────┘
src          └──────────────┘              └───────────┘
typ          └──────────────┘        └┘  └───────────┘
doc                                         └───────────┘
435    measure α :=
id     └─────┘ 
src    └─────┘
typ    └─────┘ 
436  measure.of_measurable (λ s _, m s) m.empty
id   └───────────────────┘          └────┘
src  └───────────────────┘               └────┘
typ  └───────────────────┘          └────┘
437    (λ f hf hd, m.Union_eq_of_caratheodory (λ i, h _ (hf i)) hd)
id         └┘ └┘  └───────────────────────┘          └┘    └┘
src                 └───────────────────────┘
typ        └┘ └┘  └───────────────────────┘          └┘    └┘
438  
439  lemma le_to_outer_measure_caratheodory {α} [ms : measurable_space α]
id                                                    └──────────────┘ 
src                                                   └──────────────┘
typ                                                   └──────────────┘ 
440    (μ : measure α) : ms ≤ μ.to_outer_measure.caratheodory :=
id          └─────┘     └┘  └───────────────┘└───────────┘
src         └─────┘           └───────────────┘└───────────┘
typ         └─────┘     └┘  └───────────────┘└───────────┘
doc                                             └───────────┘
441  begin
st   └─────
442    assume s hs,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid    └─────────┘
st   ────────────┘└─
443    rw to_outer_measure_eq_outer_measure',
id        └────────────────────────────────┘
src    └─┘└────────────────────────────────┘
typ    └─┘└────────────────────────────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ──────────────────────────────────────┘└─
444    refine outer_measure.caratheodory_is_measurable (λ t, le_infi $ λ ht, _),
id            └──────────────────────────────────────┘       └─────┘
src    └─────┘└──────────────────────────────────────┘  └──┘└─────┘  └─────┘
typ    └─────┘└──────────────────────────────────────┘  └──┘└─────┘  └─────┘
doc    └─────┘                                          └──┘         └─────┘
txt    └─────┘                                          └──┘         └─────┘
par    └─────┘                                          └──┘         └─────┘
pid                                                    └──┘         └─────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
445    rw [← measure_eq_measure' (ht.inter hs),
id           └─────────────────┘  └──────┘ └┘
src    └────┘└─────────────────┘ └──────┘  └──
typ    └────┘└─────────────────┘ └──────┘└┘└──
doc    └────┘                              └──
txt    └────┘                              └──
par    └────┘                              └──
pid      └──┘                              └──
st   ────────────────────────────────────────┘└─
446      ← measure_eq_measure' (ht.diff hs),
id         └─────────────────┘  └─────┘ └┘
src  ─────┘└─────────────────┘ └─────┘  └──
typ  ─────┘└─────────────────┘ └─────┘└┘└──
doc  ─────┘                             └──
txt  ─────┘                             └──
par  ─────┘                             └──
pid  ─────┘                             └──
st   ─────────────────────────────────────┘└─
447      ← measure_union _ (ht.inter hs) (ht.diff hs),
id         └───────────┘    └──────┘      └─────┘ └┘
src  ─────┘└───────────┘└─┘ └──────┘  └┘ └─────┘  └──
typ  ─────┘└───────────┘└─┘ └──────┘  └┘ └─────┘└┘└──
doc  ─────┘             └─┘           └┘          └──
txt  ─────┘             └─┘           └┘          └──
par  ─────┘             └─┘           └┘          └──
pid  ─────┘             └─┘           └┘          └──
st   ───────────────────────────────────────────────┘└─
448      inter_union_diff],
id       └──────────────┘
src  ───┘└──────────────┘
typ  ───┘└──────────────┘
doc  ───┘                
txt  ───┘                
par  ───┘                
pid  ───┘                
st   ───────────────────┘└──
449    exact le_refl _,
id           └─────┘
src    └────┘└─────┘└┘
typ    └────┘└─────┘└┘
doc    └────┘       └┘
txt    └────┘       └┘
par    └────┘       └┘
pid                └┘
st   ────────────────┘└─
450    exact λ x ⟨⟨_, h₁⟩, _, h₂⟩, h₂ h₁
id                    └┘      └┘
src    └────┘ └──┘ └─┘  └────┘  └─┘    
typ    └────┘ └──┘ └─┘└┘└────┘└┘└─┘    
doc    └────┘ └──┘ └─┘  └────┘  └─┘    
txt    └────┘ └──┘ └─┘  └────┘  └─┘    
par    └────┘ └──┘ └─┘  └────┘  └─┘    
pid          └──┘ └─┘  └────┘  └─┘    
st   ───────────────────────────────────┘
451  end
st   └─┘
452  
453  lemma to_measure_to_outer_measure {α} (m : outer_measure α)
id                                              └───────────┘ 
src                                             └───────────┘
typ                                             └───────────┘ 
454    [ms : measurable_space α] (h : ms ≤ m.caratheodory) :
id           └──────────────┘        └┘  └───────────┘
src          └──────────────┘              └───────────┘
typ          └──────────────┘        └┘  └───────────┘
doc                                         └───────────┘
455    (m.to_measure h).to_outer_measure = m.trim := rfl
id      └─────────┘  └──────────────┘   └───┘    └─┘
src      └─────────┘   └──────────────┘    └───┘    └─┘
typ     └─────────┘  └──────────────┘   └───┘    └─┘
456  
457  @[simp] lemma to_measure_apply {α} (m : outer_measure α)
id                                           └───────────┘ 
src                                          └───────────┘
typ                                          └───────────┘ 
doc    └──┘
458    [ms : measurable_space α] (h : ms ≤ m.caratheodory)
id           └──────────────┘        └┘  └───────────┘
src          └──────────────┘              └───────────┘
typ          └──────────────┘        └┘  └───────────┘
doc                                         └───────────┘
459    {s : set α} (hs : is_measurable s) :
id          └─┘         └───────────┘ 
src         └─┘          └───────────┘
typ         └─┘         └───────────┘ 
doc                      └───────────┘
460    m.to_measure h s = m s := m.trim_eq hs
id     └─────────┘         └──────┘ └┘
src     └─────────┘              └──────┘
typ    └─────────┘         └──────┘ └┘
461  
462  lemma to_outer_measure_to_measure {α : Type*} [ms : measurable_space α] {μ : measure α} :
id                                                       └──────────────┘        └─────┘ 
src                                                      └──────────────┘         └─────┘
typ                                                      └──────────────┘        └─────┘ 
463    μ.to_outer_measure.to_measure (le_to_outer_measure_caratheodory _) = μ :=
id     └───────────────┘└─────────┘  └──────────────────────────────┘     
src     └───────────────┘└─────────┘  └──────────────────────────────┘    
typ    └───────────────┘└─────────┘  └──────────────────────────────┘     
464  measure.ext $ λ s, μ.to_outer_measure.trim_eq
id   └─────────┘       └───────────────┘└──────┘
src  └─────────┘         └───────────────┘└──────┘
typ  └─────────┘       └───────────────┘└──────┘
465  
466  namespace measure
467  variables {α : Type*} {β : Type*} {γ : Type*}
id             
typ            
468    [measurable_space α] [measurable_space β] [measurable_space γ]
id      └──────────────┘     └──────────────┘     └──────────────┘
src     └──────────────┘     └──────────────┘     └──────────────┘
typ     └──────────────┘     └──────────────┘     └──────────────┘
469  
470  instance : has_zero (measure α) :=
id              └──────┘  └─────┘ 
src             └──────┘  └─────┘
typ             └──────┘  └─────┘ 
471  ⟨{ to_outer_measure := 0,
472     m_Union := λ f hf hd, tsum_zero.symm,
id                    └┘ └┘  └───────┘└───┘
src                           └───────┘└───┘
typ                   └┘ └┘  └───────┘└───┘
473     trimmed := outer_measure.trim_zero }⟩
id                 └─────────────────────┘
src                └─────────────────────┘
typ                └─────────────────────┘
474  
475  @[simp] theorem zero_to_outer_measure :
doc    └──┘
476    (0 : measure α).to_outer_measure = 0 := rfl
id          └─────┘  └──────────────┘        └─┘
src         └─────┘   └──────────────┘        └─┘
typ         └─────┘  └──────────────┘        └─┘
477  
478  @[simp] theorem zero_apply (s : set α) : (0 : measure α) s = 0 := rfl
id                                   └─┘          └─────┘          └─┘
src                                  └─┘           └─────┘            └─┘
typ                                  └─┘          └─────┘          └─┘
doc    └──┘
479  
480  instance : inhabited (measure α) := ⟨0⟩
id              └───────┘  └─────┘ 
src             └───────┘  └─────┘
typ             └───────┘  └─────┘ 
481  
482  instance : has_add (measure α) :=
id              └─────┘  └─────┘ 
src             └─────┘  └─────┘
typ             └─────┘  └─────┘ 
483  ⟨λμ₁ μ₂, {
id     └┘ └┘
typ    └┘ └┘
484    to_outer_measure := μ₁.to_outer_measure + μ₂.to_outer_measure,
id                         └┘└───────────────┘  └┘└───────────────┘
src                          └───────────────┘    └───────────────┘
typ                        └┘└───────────────┘  └┘└───────────────┘
485    m_Union := λs hs hd,
id                  └┘ └┘
typ                 └┘ └┘
486      show μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑ i, μ₁ (s i) + μ₂ (s i),
id            └┘        └┘          └┘      └┘   
src                                                 
typ           └┘        └┘          └┘      └┘   
doc                                         
487      by rw [ennreal.tsum_add, measure_Union hd hs, measure_Union hd hs],
id              └──────────────┘  └───────────┘ └┘ └┘  └───────────┘ └┘ └┘
src         └──┘└──────────────┘└┘└───────────┘    └┘└───────────┘    
typ         └──┘└──────────────┘└┘└───────────┘└┘└┘└┘└───────────┘└┘└┘
doc         └──┘                └┘                 └┘                 
txt         └──┘                └┘                 └┘                 
par         └──┘                └┘                 └┘                 
pid           └┘                └┘                 └┘                 
st         └───────────────────┘└───────────────────┘└───────────────────┘
488    trimmed := by rw [outer_measure.trim_add, μ₁.trimmed, μ₂.trimmed] }⟩
id                       └────────────────────┘
src                  └──┘└────────────────────┘└┘          └┘          └┘
typ                  └──┘└────────────────────┘└┘└────────┘└┘└────────┘└┘
doc                  └──┘                      └┘          └┘          └┘
txt                  └──┘                      └┘          └┘          └┘
par                  └──┘                      └┘          └┘          └┘
pid                    └┘                      └┘          └┘          
st                  └─────────────────────────┘└──────────┘└──────────┘
489  
490  @[simp] theorem add_to_outer_measure (μ₁ μ₂ : measure α) :
id                                                 └─────┘ 
src                                                └─────┘
typ                                                └─────┘ 
doc    └──┘
491    (μ₁ + μ₂).to_outer_measure = μ₁.to_outer_measure + μ₂.to_outer_measure := rfl
id      └┘  └┘ └──────────────┘   └┘└───────────────┘  └┘└───────────────┘    └─┘
src            └──────────────┘     └───────────────┘    └───────────────┘    └─┘
typ     └┘  └┘ └──────────────┘   └┘└───────────────┘  └┘└───────────────┘    └─┘
492  
493  @[simp] theorem add_apply (μ₁ μ₂ : measure α) (s : set α) :
id                                      └─────┘        └─┘ 
src                                     └─────┘         └─┘
typ                                     └─────┘        └─┘ 
doc    └──┘
494    (μ₁ + μ₂) s = μ₁ s + μ₂ s := rfl
id      └┘  └┘    └┘   └┘     └─┘
src                              └─┘
typ     └┘  └┘    └┘   └┘     └─┘
495  
496  instance add_comm_monoid : add_comm_monoid (measure α) :=
id                              └─────────────┘  └─────┘ 
src                             └─────────────┘  └─────┘
typ                             └─────────────┘  └─────┘ 
497  { zero      := 0,
498    add       := (+),
id                  
src                 
typ                 
499    add_assoc := assume a b c, ext $ assume s hs, add_assoc _ _ _,
id                             └─┘           └┘  └───────┘
src                               └─┘                └───────┘
typ                            └─┘           └┘  └───────┘
500    add_comm  := assume a b, ext $ assume s hs, add_comm _ _,
id                            └─┘           └┘  └──────┘
src                             └─┘                └──────┘
typ                           └─┘           └┘  └──────┘
501    zero_add  := assume a, ext $ assume s hs, zero_add _,
id                           └─┘           └┘  └──────┘
src                           └─┘                └──────┘
typ                          └─┘           └┘  └──────┘
502    add_zero  := assume a, ext $ assume s hs, add_zero _ }
id                           └─┘           └┘  └──────┘
src                           └─┘                └──────┘
typ                          └─┘           └┘  └──────┘
503  
504  instance : partial_order (measure α) :=
id              └───────────┘  └─────┘ 
src             └───────────┘  └─────┘
typ             └───────────┘  └─────┘ 
505  { le          := λm₁ m₂, ∀ s, is_measurable s → m₁ s ≤ m₂ s,
id                    └┘ └┘      └───────────┘    └┘   └┘ 
src                               └───────────┘          
typ                   └┘ └┘      └───────────┘    └┘   └┘ 
doc                                └───────────┘
506    le_refl     := assume m s hs, le_refl _,
id                             └┘  └─────┘
src                                  └─────┘
typ                            └┘  └─────┘
507    le_trans    := assume m₁ m₂ m₃ h₁ h₂ s hs, le_trans (h₁ s hs) (h₂ s hs),
id                           └┘ └┘ └┘ └┘ └┘  └┘  └──────┘  └┘  └┘   └┘  └┘
src                                               └──────┘
typ                          └┘ └┘ └┘ └┘ └┘  └┘  └──────┘  └┘  └┘   └┘  └┘
508    le_antisymm := assume m₁ m₂ h₁ h₂, ext $
id                           └┘ └┘ └┘ └┘  └─┘
src                                       └─┘
typ                          └┘ └┘ └┘ └┘  └─┘
509      assume s hs, le_antisymm (h₁ s hs) (h₂ s hs) }
id               └┘  └─────────┘  └┘  └┘   └┘  └┘
src                   └─────────┘
typ              └┘  └─────────┘  └┘  └┘   └┘  └┘
510  
511  theorem le_iff {μ₁ μ₂ : measure α} :
id                           └─────┘ 
src                          └─────┘
typ                          └─────┘ 
512    μ₁ ≤ μ₂ ↔ ∀ s, is_measurable s → μ₁ s ≤ μ₂ s := iff.rfl
id     └┘  └┘      └───────────┘    └┘   └┘     └─────┘
src                 └───────────┘                   └─────┘
typ    └┘  └┘      └───────────┘    └┘   └┘     └─────┘
doc                   └───────────┘
513  
514  theorem to_outer_measure_le {μ₁ μ₂ : measure α} :
id                                        └─────┘ 
src                                       └─────┘
typ                                       └─────┘ 
515    μ₁.to_outer_measure ≤ μ₂.to_outer_measure ↔ μ₁ ≤ μ₂ :=
id     └┘└───────────────┘  └┘└───────────────┘  └┘  └┘
src      └───────────────┘    └───────────────┘     
typ    └┘└───────────────┘  └┘└───────────────┘  └┘  └┘
516  by rw [← μ₂.trimmed, outer_measure.le_trim_iff]; refl
id                        └───────────────────────┘
src     └────┘          └┘└───────────────────────┘  └────
typ     └────┘└────────┘└┘└───────────────────────┘  └────
doc     └────┘          └┘                           └────
txt     └────┘          └┘                           └────
par     └────┘          └┘                           └────
pid       └──┘          └┘                               
st     └───────────────┘└─────────────────────────┘└──────
517  
src  
typ  
doc  
txt  
par  
pid  
st   
518  theorem le_iff' {μ₁ μ₂ : measure α} :
id                            └─────┘ 
src                           └─────┘
typ                           └─────┘ 
519    μ₁ ≤ μ₂ ↔ ∀ s, μ₁ s ≤ μ₂ s :=
id     └┘  └┘      └┘   └┘ 
src                      
typ    └┘  └┘      └┘   └┘ 
520  to_outer_measure_le.symm
id   └─────────────────┘└───┘
src  └─────────────────┘└───┘
typ  └─────────────────┘└───┘
521  
522  section
523  variables {m : set (measure α)} {μ : measure α}
id                  └─┘  └─────┘          └─────┘
src                 └─┘  └─────┘          └─────┘
typ                 └─┘  └─────┘          └─────┘
524  
525  lemma Inf_caratheodory (s : set α) (hs : is_measurable s) :
id                               └─┘         └───────────┘ 
src                              └─┘          └───────────┘
typ                              └─┘         └───────────┘ 
doc                                           └───────────┘
526    (Inf (measure.to_outer_measure '' m)).caratheodory.is_measurable s :=
id      └─┘  └──────────────────────┘ └┘   └──────────┘ └───────────┘  
src     └─┘  └──────────────────────┘ └┘    └──────────┘ └───────────┘
typ     └─┘  └──────────────────────┘ └┘   └──────────┘ └───────────┘  
doc     └─┘                                 └──────────┘
527  begin
st   └─────
528    rw [outer_measure.Inf_eq_of_function_Inf_gen],
id         └──────────────────────────────────────┘
src    └──┘└──────────────────────────────────────┘
typ    └──┘└──────────────────────────────────────┘
doc    └──┘                                        
txt    └──┘                                        
par    └──┘                                        
pid      └┘                                        
st   ─────────────────────────────────────────────┘└──
529    refine outer_measure.caratheodory_is_measurable (assume t, _),
id            └──────────────────────────────────────┘
src    └─────┘└──────────────────────────────────────┘       └────┘
typ    └─────┘└──────────────────────────────────────┘       └────┘
doc    └─────┘                                               └────┘
txt    └─────┘                                               └────┘
par    └─────┘                                               └────┘
pid                                                         └────┘
st   ──────────────────────────────────────────────────────────────┘└─
530    cases t.eq_empty_or_nonempty with ht ht, by simp [ht],
id           └────────────────────┘                      └┘
src    └────┘└────────────────────┘└─────────┘     └────┘  
typ    └────┘└────────────────────┘└─────────┘     └────┘└┘
doc    └────┘                      └─────────┘     └────┘  
txt    └────┘                      └─────────┘     └────┘  
par    └────┘                      └─────────┘     └────┘  
pid                               └─────────┘           
st   ────────────────────────────────────────┘              └─
531    simp only [outer_measure.Inf_gen_nonempty1 _ _ ht, le_infi_iff, ball_image_iff,
id                └─────────────────────────────┘     └┘  └─────────┘  └────────────┘
src    └─────────┘└─────────────────────────────┘└───┘  └┘└─────────┘└┘└────────────┘└─
typ    └─────────┘└─────────────────────────────┘└───┘└┘└┘└─────────┘└┘└────────────┘└─
doc    └─────────┘                               └───┘  └┘           └┘              └─
txt    └─────────┘                               └───┘  └┘           └┘              └─
par    └─────────┘                               └───┘  └┘           └┘              └─
pid        └──┘└┘                               └───┘  └┘           └┘              └─
st   ──────────────────────────────────────────────────────────────────────────────────
532      to_outer_measure_apply, measure_eq_infi t],
id       └────────────────────┘  └─────────────┘ 
src  ───┘└────────────────────┘└┘└─────────────┘ 
typ  ───┘└────────────────────┘└┘└─────────────┘
doc  ───┘                      └┘                
txt  ───┘                      └┘                
par  ───┘                      └┘                
pid  ───┘                      └┘                
st   ─────────────────────────────────────────────┘└─
533    assume μ hμ u htu hu,
src    └──────────────────┘
typ    └──────────────────┘
doc    └──────────────────┘
txt    └──────────────────┘
par    └──────────────────┘
pid    └──────────────────┘
st   ─────────────────────┘└─
534    have hm : ∀{s t}, s ⊆ t → outer_measure.Inf_gen (to_outer_measure '' m) s ≤ μ t,
id                              └───────────────────┘  └──────────────┘ └┘      
src    └────────┘ └───┘    └───────────────────┘ └──────────────┘└┘ └┘  
typ    └────────┘ └───┘    └───────────────────┘ └──────────────┘└┘└┘ 
doc    └────────┘ └───┘                                              └┘   
txt    └────────┘ └───┘                                              └┘   
par    └────────┘ └───┘                                              └┘   
pid    └─────┘└─┘ └───┘                                              └┘   
st   ────────────────────────────────────────────────────────────────────────────────┘└─
535    { assume s t hst,
src      └────────────┘
typ      └────────────┘
doc      └────────────┘
txt      └────────────┘
par      └────────────┘
pid      └────────────┘
st   ───┘└────────────┘└─
536      rw [outer_measure.Inf_gen_nonempty2 _ _ (mem_image_of_mem _ hμ)],
id           └─────────────────────────────┘      └──────────────┘   └┘
src      └──┘└─────────────────────────────┘└───┘ └──────────────┘└─┘  └┘
typ      └──┘└─────────────────────────────┘└───┘ └──────────────┘└─┘└┘└┘
doc      └──┘                               └───┘                 └─┘  └┘
txt      └──┘                               └───┘                 └─┘  └┘
par      └──┘                               └───┘                 └─┘  └┘
pid        └┘                               └───┘                 └─┘  └┘
st   ──────────────────────────────────────────────────────────────────┘└──
537      refine infi_le_of_le (μ.to_outer_measure) (infi_le_of_le (mem_image_of_mem _ hμ) _),
id                             └────────────────┘   └───────────┘  └──────────────┘   └┘
src      └─────┘              └────────────────┘└┘ └───────────┘ └──────────────┘└─┘  └──┘
typ      └─────┘              └────────────────┘└┘ └───────────┘ └──────────────┘└─┘└┘└──┘
doc      └─────┘                                └┘                               └─┘  └──┘
txt      └─────┘                                └┘                               └─┘  └──┘
par      └─────┘                                └┘                               └─┘  └──┘
pid                                            └┘                               └─┘  └──┘
st   ──────────────────────────────────────────────────────────────────────────────────────┘└─
538      rw [to_outer_measure_apply],
id           └────────────────────┘
src      └──┘└────────────────────┘
typ      └──┘└────────────────────┘
doc      └──┘                      
txt      └──┘                      
par      └──┘                      
pid        └┘                      
st   ─────────────────────────────┘└──
539      refine measure_mono hst },
id              └──────────┘ └─┘
src      └─────┘└──────────┘   
typ      └─────┘└──────────┘└─┘
doc      └─────┘               
txt      └─────┘               
par      └─────┘               
pid                           
st   ───────────────────────────┘└┘
540    rw [measure_eq_inter_diff hu hs],
id         └───────────────────┘ └┘ └┘
src    └──┘└───────────────────┘    
typ    └──┘└───────────────────┘└┘└┘
doc    └──┘                         
txt    └──┘                         
par    └──┘                         
pid      └┘                         
st   ────────────────────────────────┘└──
541    refine add_le_add' (hm $ inter_subset_inter_left _ htu) (hm $ diff_subset_diff_left htu)
id            └─────────┘       └─────────────────────┘         └┘   └───────────────────┘ └─┘
src    └─────┘└─────────┘    └─────────────────────┘└─┘   └┘    └───────────────────┘   └┘
typ    └─────┘└─────────┘    └─────────────────────┘└─┘   └┘ └┘ └───────────────────┘└─┘└┘
doc    └─────┘                                      └─┘   └┘                            └┘
txt    └─────┘                                      └─┘   └┘                            └┘
par    └─────┘                                      └─┘   └┘                            └┘
pid                                                └─┘   └┘                            
st   ──────────────────────────────────────────────────────────────────────────────────────────┘
542  end
st   └─┘
543  
544  instance : has_Inf (measure α) :=
id              └─────┘  └─────┘ 
src             └─────┘  └─────┘
typ             └─────┘  └─────┘ 
doc             └─────┘
545  ⟨λm, (Inf (to_outer_measure '' m)).to_measure $ Inf_caratheodory⟩
id        └─┘  └──────────────┘ └┘   └────────┘    └──────────────┘
src        └─┘  └──────────────┘ └┘    └────────┘    └──────────────┘
typ       └─┘  └──────────────┘ └┘   └────────┘    └──────────────┘
doc        └─┘
546  
547  lemma Inf_apply {m : set (measure α)} {s : set α} (hs : is_measurable s) :
id                        └─┘  └─────┘         └─┘         └───────────┘ 
src                       └─┘  └─────┘          └─┘          └───────────┘
typ                       └─┘  └─────┘         └─┘         └───────────┘ 
doc                                                          └───────────┘
548    Inf m s = Inf (to_outer_measure '' m) s :=
id     └─┘    └─┘  └──────────────┘ └┘   
src    └─┘      └─┘  └──────────────┘ └┘
typ    └─┘    └─┘  └──────────────┘ └┘   
doc    └─┘       └─┘
549  to_measure_apply _ _ hs
id   └──────────────┘     └┘
src  └──────────────┘
typ  └──────────────┘     └┘
550  
551  private lemma Inf_le (h : μ ∈ m) : Inf m ≤ μ :=
id                                   └─┘   
src                                    └─┘   
typ                                  └─┘   
doc                                     └─┘
552  have Inf (to_outer_measure '' m) ≤ μ.to_outer_measure := Inf_le (mem_image_of_mem _ h),
id        └─┘  └──────────────┘ └┘    └───────────────┘    └────┘  └──────────────┘   
src       └─┘  └──────────────┘ └┘      └───────────────┘    └────┘  └──────────────┘
typ       └─┘  └──────────────┘ └┘    └───────────────┘    └────┘  └──────────────┘   
doc       └─┘
553  assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s
id           └┘         └───────┘ └┘    └────────────────────┘         └──┘ 
src                  └──┘└───────┘  └──┘└────────────────────┘  └────┘     
typ          └┘     └──┘└───────┘└┘└──┘└────────────────────┘  └────┘└──┘
doc                  └──┘           └──┘                        └────┘     
txt                  └──┘           └──┘                        └────┘     
par                  └──┘           └──┘                        └────┘     
pid                    └┘           └──┘                                  
st                  └───────────────┘└────────────────────────┘└──────────────
554  
src  
typ  
doc  
txt  
par  
pid  
st   
555  private lemma le_Inf (h : ∀μ' ∈ m, μ ≤ μ') : μ ≤ Inf m :=
id                              └┘       └┘      └─┘ 
src                                                 └─┘
typ                             └┘       └┘      └─┘ 
doc                                                   └─┘
556  have μ.to_outer_measure ≤ Inf (to_outer_measure '' m) :=
id        └───────────────┘  └─┘  └──────────────┘ └┘ 
src        └───────────────┘  └─┘  └──────────────┘ └┘
typ       └───────────────┘  └─┘  └──────────────┘ └┘ 
doc                            └─┘
557    le_Inf $ ball_image_of_ball $ assume μ hμ, to_outer_measure_le.2 $ h _ hμ,
id     └────┘   └────────────────┘           └┘  └─────────────────┘       └┘
src    └────┘   └────────────────┘                └─────────────────┘
typ    └────┘   └────────────────┘           └┘  └─────────────────┘       └┘
558  assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s
id           └┘         └───────┘ └┘    └────────────────────┘         └──┘ 
src                  └──┘└───────┘  └──┘└────────────────────┘  └────┘     
typ          └┘     └──┘└───────┘└┘└──┘└────────────────────┘  └────┘└──┘
doc                  └──┘           └──┘                        └────┘     
txt                  └──┘           └──┘                        └────┘     
par                  └──┘           └──┘                        └────┘     
pid                    └┘           └──┘                                  
st                  └───────────────┘└────────────────────────┘└──────────────
559  
src  
typ  
doc  
txt  
par  
pid  
st   
560  instance : has_Sup (measure α) := ⟨λs, Inf {μ' | ∀μ∈s, μ ≤ μ' }⟩
id              └─────┘  └─────┘          └─┘ └┘         └┘
src             └─────┘  └─────┘            └─┘              
typ             └─────┘  └─────┘          └─┘ └┘         └┘
doc             └─────┘                     └─┘
561  private lemma le_Sup (h : μ ∈ m) : μ ≤ Sup m := le_Inf $ assume μ' h', h' _ h
id                                     └─┘     └────┘          └┘ └┘  └┘   
src                                       └─┘      └────┘
typ                                    └─┘     └────┘          └┘ └┘  └┘   
doc                                         └─┘
562  private lemma Sup_le (h : ∀μ' ∈ m, μ' ≤ μ) : Sup m ≤ μ := Inf_le h
id                              └┘     └┘      └─┘       └────┘ 
src                                              └─┘         └────┘
typ                             └┘     └┘      └─┘       └────┘ 
doc                                               └─┘
563  
564  instance : order_bot (measure α) :=
id              └───────┘  └─────┘ 
src             └───────┘  └─────┘
typ             └───────┘  └─────┘ 
doc             └───────┘
565  { bot := 0, bot_le := assume a s hs, bot_le, .. measure.partial_order }
id                                  └┘  └────┘     └───────────────────┘
src                                       └────┘     └───────────────────┘
typ                                 └┘  └────┘     └───────────────────┘
566  
567  instance : order_top (measure α) :=
id              └───────┘  └─────┘ 
src             └───────┘  └─────┘
typ             └───────┘  └─────┘ 
doc             └───────┘
568  { top := (⊤ : outer_measure α).to_measure (by rw [outer_measure.top_caratheodory]; exact le_top),
id                └───────────┘  └────────┘          └────────────────────────────┘         └────┘
src               └───────────┘   └────────┘      └──┘└────────────────────────────┘  └────┘└────┘
typ               └───────────┘  └────────┘      └──┘└────────────────────────────┘  └────┘└────┘
doc                                                └──┘                                └────┘
txt                                                └──┘                                └────┘
par                                                └──┘                                └────┘
pid                                                  └┘                                     
st                                                └─────────────────────────────────┘└────────────┘
569    le_top := assume a s hs,
id                        └┘
typ                       └┘
570      by cases s.eq_empty_or_nonempty with h  h;
id                └────────────────────┘
src         └────┘└────────────────────┘└────────┘
typ         └────┘└────────────────────┘└────────┘
doc         └────┘                      └────────┘
txt         └────┘                      └────────┘
par         └────┘                      └────────┘
pid                                    └────────┘
st         └────────────────────────────────────────
571        simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply],
id                 └──────────────┘    └┘  └─────────────────────┘
src        └────┘ └┘└──────────────┘└─┘  └┘└─────────────────────┘
typ        └────┘└┘└──────────────┘└─┘└┘└┘└─────────────────────┘
doc        └────┘ └┘                 └─┘  └┘                       
txt        └────┘ └┘                 └─┘  └┘                       
par        └────┘ └┘                 └─┘  └┘                       
pid             └┘                 └─┘  └┘                       
st   ───────────────────────────────────────────────────────────────┘
572    .. measure.partial_order }
id        └───────────────────┘
src       └───────────────────┘
typ       └───────────────────┘
573  
574  instance : complete_lattice (measure α) :=
id              └──────────────┘  └─────┘ 
src             └──────────────┘  └─────┘
typ             └──────────────┘  └─────┘ 
doc             └──────────────┘
575  { Inf          := Inf,
id                     └─┘
src                    └─┘
typ                    └─┘
doc                    └─┘
576    Sup          := Sup,
id                     └─┘
src                    └─┘
typ                    └─┘
doc                    └─┘
577    inf          := λa b, Inf {a, b},
id                         └─┘  
src                          └─┘  
typ                        └─┘  
doc                          └─┘
578    sup          := λa b, Sup {a, b},
id                         └─┘  
src                          └─┘  
typ                        └─┘  
doc                          └─┘
579    le_Sup       := assume s μ h, le_Sup h,
id                                └────┘ 
src                                  └────┘
typ                               └────┘ 
580    Sup_le       := assume s μ h, Sup_le h,
id                                └────┘ 
src                                  └────┘
typ                               └────┘ 
581    Inf_le       := assume s μ h, Inf_le h,
id                                └────┘ 
src                                  └────┘
typ                               └────┘ 
582    le_Inf       := assume s μ h, le_Inf h,
id                                └────┘ 
src                                  └────┘
typ                               └────┘ 
583    le_sup_left  := assume a b, le_Sup $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
584    le_sup_right := assume a b, le_Sup $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
585    sup_le       := assume a b c hac hbc, Sup_le $ by simp [*, or_imp_distrib] {contextual := tt},
id                               └─┘ └─┘  └────┘               └────────────┘                 └┘
src                                          └────┘      └───────┘└────────────┘└┘ └────────────┘└┘
typ                              └─┘ └─┘  └────┘      └───────┘└────────────┘└┘ └────────────┘└┘
doc                                                      └───────┘              └┘ └────────────┘  
txt                                                      └───────┘              └┘ └────────────┘  
par                                                      └───────┘              └┘ └────────────┘  
pid                                                          └──┘               └────────────┘  
st                                                      └──────────────────────────────────────────┘
586    inf_le_left  := assume a b, Inf_le $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
587    inf_le_right := assume a b, Inf_le $ by simp,
id                               └────┘
src                                └────┘      └──┘
typ                              └────┘      └──┘
doc                                            └──┘
txt                                            └──┘
par                                            └──┘
st                                            └───┘
588    le_inf       := assume a b c hac hbc, le_Inf $ by simp [*, or_imp_distrib] {contextual := tt},
id                               └─┘ └─┘  └────┘               └────────────┘                 └┘
src                                          └────┘      └───────┘└────────────┘└┘ └────────────┘└┘
typ                              └─┘ └─┘  └────┘      └───────┘└────────────┘└┘ └────────────┘└┘
doc                                                      └───────┘              └┘ └────────────┘  
txt                                                      └───────┘              └┘ └────────────┘  
par                                                      └───────┘              └┘ └────────────┘  
pid                                                          └──┘               └────────────┘  
st                                                      └──────────────────────────────────────────┘
589    .. measure.partial_order, .. measure.lattice.order_top, .. measure.lattice.order_bot }
id        └───────────────────┘     └───────────────────────┘     └───────────────────────┘
src       └───────────────────┘     └───────────────────────┘     └───────────────────────┘
typ       └───────────────────┘     └───────────────────────┘     └───────────────────────┘
590  
591  end
592  
593  def map (f : α → β) (μ : measure α) : measure β :=
id                          └─────┘     └─────┘ 
src                           └─────┘      └─────┘
typ                         └─────┘     └─────┘ 
594  if hf : measurable f then
id   └┘      └────────┘ 
src  └┘      └────────┘
typ  └┘      └────────┘ 
doc          └────────┘
595    (μ.to_outer_measure.map f).to_measure $ λ s hs t,
id      └───────────────┘└──┘  └────────┘       └┘ 
src      └───────────────┘└──┘   └────────┘
typ     └───────────────┘└──┘  └────────┘       └┘ 
596    le_to_outer_measure_caratheodory μ _ (hf _ hs) (f ⁻¹' t)
id     └──────────────────────────────┘     └┘   └┘    └─┘ 
src    └──────────────────────────────┘                  └─┘
typ    └──────────────────────────────┘     └┘   └┘    └─┘ 
doc                                                      └─┘
597  else 0
id        
src       
typ       
598  
599  variables {μ ν : measure α}
id                    └─────┘
src                   └─────┘
typ                   └─────┘
600  
601  @[simp] theorem map_apply {f : α → β} (hf : measurable f)
id                                             └────────┘ 
src                                              └────────┘
typ                                            └────────┘ 
doc    └──┘                                      └────────┘
602    {s : set β} (hs : is_measurable s) :
id          └─┘         └───────────┘ 
src         └─┘          └───────────┘
typ         └─┘         └───────────┘ 
doc                      └───────────┘
603    (map f μ : measure β) s = μ (f ⁻¹' s) :=
id      └─┘     └─────┘        └─┘ 
src     └─┘       └─────┘            └─┘
typ     └─┘     └─────┘        └─┘ 
doc                                   └─┘
604  by rw [map, dif_pos hf, to_measure_apply _ _ hs]; refl
id          └─┘  └─────┘ └┘  └──────────────┘     └┘
src     └──┘└─┘└┘└─────┘  └┘└──────────────┘└───┘    └────
typ     └──┘└─┘└┘└─────┘└┘└┘└──────────────┘└───┘└┘  └────
doc     └──┘   └┘         └┘                └───┘    └────
txt     └──┘   └┘         └┘                └───┘    └────
par     └──┘   └┘         └┘                └───┘    └────
pid       └┘   └┘         └┘                └───┘        
st     └──────┘└──────────┘└───────────────────────┘└──────
605  
src  
typ  
doc  
txt  
par  
pid  
st   
606  @[simp] lemma map_id : map id μ = μ :=
id                          └─┘ └┘   
src                         └─┘ └┘   
typ                         └─┘ └┘   
doc    └──┘
607  ext $ λ s, map_apply measurable_id
id   └─┘       └───────┘ └───────────┘
src  └─┘        └───────┘ └───────────┘
typ  └─┘       └───────┘ └───────────┘
608  
609  lemma map_map {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) :
id                                           └────────┘         └────────┘ 
src                                              └────────┘          └────────┘
typ                                          └────────┘         └────────┘ 
doc                                              └────────┘          └────────┘
610    map g (map f μ) = map (g ∘ f) μ :=
id     └─┘   └─┘     └─┘      
src    └─┘    └─┘       └─┘    
typ    └─┘   └─┘     └─┘      
611  ext $ λ s hs,
id   └─┘      └┘
src  └─┘
typ  └─┘      └┘
612  by simp [hf, hg, hs, hg.preimage hs, hg.comp hf];
id            └┘  └┘  └┘  └─────────┘ └┘  └─────┘ └┘
src     └────┘  └┘  └┘  └┘└─────────┘  └┘└─────┘  
typ     └────┘└┘└┘└┘└┘└┘└┘└─────────┘└┘└┘└─────┘└┘
doc     └────┘  └┘  └┘  └┘             └┘         
txt     └────┘  └┘  └┘  └┘             └┘         
par     └────┘  └┘  └┘  └┘             └┘         
pid           └┘  └┘  └┘             └┘         
st     └───────────────────────────────────────────────
613     rw ← preimage_comp
id           └───────────┘
src     └───┘└───────────┘
typ     └───┘└───────────┘
doc     └───┘             
txt     └───┘             
par     └───┘             
pid       └─┘             
st   ──────────────────────
614  
src  
typ  
doc  
txt  
par  
pid  
st   
615  /-- The dirac measure. -/
616  def dirac (a : α) : measure α :=
id                      └─────┘ 
src                      └─────┘
typ                     └─────┘ 
617  (outer_measure.dirac a).to_measure (by simp)
id    └─────────────────┘  └────────┘
src   └─────────────────┘   └────────┘      └──┘
typ   └─────────────────┘  └────────┘      └──┘
doc   └─────────────────┘                   └──┘
txt                                         └──┘
par                                         └──┘
st                                         └───┘
618  
619  @[simp] lemma dirac_apply (a : α) {s : set α} (hs : is_measurable s) :
id                                         └─┘         └───────────┘ 
src                                         └─┘          └───────────┘
typ                                        └─┘         └───────────┘ 
doc    └──┘                                              └───────────┘
620    (dirac a : measure α) s = ⨆ h : a ∈ s, 1 :=
id      └───┘    └─────┘            
src     └───┘     └─────┘                
typ     └───┘    └─────┘            
doc     └───┘                              
621  to_measure_apply _ _ hs
id   └──────────────┘     └┘
src  └──────────────┘
typ  └──────────────┘     └┘
622  
623  /-- Sum of an indexed family of measures. -/
624  def sum {ι : Type*} (f : ι → measure α) : measure α :=
id                               └─────┘     └─────┘ 
src                               └─────┘      └─────┘
typ                              └─────┘     └─────┘ 
625  (outer_measure.sum (λ i, (f i).to_outer_measure)).to_measure $
id    └───────────────┘         └──────────────┘   └────────┘
src   └───────────────┘            └──────────────┘   └────────┘
typ   └───────────────┘         └──────────────┘   └────────┘
626  le_trans
id   └──────┘
src  └──────┘
typ  └──────┘
627    (by exact le_infi (λ i, le_to_outer_measure_caratheodory _))
id               └─────┘       └──────────────────────────────┘
src        └────┘└─────┘  └──┘└──────────────────────────────┘└─┘
typ        └────┘└─────┘  └──┘└──────────────────────────────┘└─┘
doc        └────┘         └──┘                                └─┘
txt        └────┘         └──┘                                └─┘
par        └────┘         └──┘                                └─┘
pid                      └──┘                                └─┘
st        └──────────────────────────────────────────────────────┘
628    (outer_measure.le_sum_caratheodory _)
id      └───────────────────────────────┘
src     └───────────────────────────────┘
typ     └───────────────────────────────┘
629  
630  /-- Counting measure on any measurable space. -/
631  def count : measure α := sum dirac
id               └─────┘     └─┘ └───┘
src              └─────┘      └─┘ └───┘
typ              └─────┘     └─┘ └───┘
doc                           └─┘ └───┘
632  
633  @[class] def is_complete {α} {_:measurable_space α} (μ : measure α) : Prop :=
id                                   └──────────────┘        └─────┘ 
src                                  └──────────────┘         └─────┘
typ                                  └──────────────┘        └─────┘ 
634  ∀ s, μ s = 0 → is_measurable s
id              └───────────┘ 
src                └───────────┘
typ             └───────────┘ 
doc                 └───────────┘
635  
636  /-- The "almost everywhere" filter of co-null sets. -/
637  def a_e (μ : measure α) : filter α :=
id                └─────┘     └────┘ 
src               └─────┘      └────┘
typ               └─────┘     └────┘ 
638  { sets := {s | μ (-s) = 0},
id                    
src                      
typ                   
639    univ_sets := by simp [measure_empty],
id                           └───────────┘
src                    └────┘└───────────┘
typ                    └────┘└───────────┘
doc                    └────┘             
txt                    └────┘             
par                    └────┘             
pid                                     
st                    └───────────────────┘
640    inter_sets := λ s t hs ht, by simp [compl_inter]; exact measure_union_null hs ht,
id                       └┘ └┘           └─────────┘         └────────────────┘ └┘ └┘
src                                  └────┘└─────────┘  └────┘└────────────────┘  
typ                      └┘ └┘     └────┘└─────────┘  └────┘└────────────────┘└┘└┘
doc                                  └────┘             └────┘                    
txt                                  └────┘             └────┘                    
par                                  └────┘             └────┘                    
pid                                                                            
st                                  └─────────────────────────────────────────────────┘
641    sets_of_superset := λ s t hs hst, measure_mono_null (set.compl_subset_compl.2 hst) hs }
id                             └┘ └─┘  └───────────────┘  └────────────────────┘  └─┘  └┘
src                                      └───────────────┘  └────────────────────┘
typ                            └┘ └─┘  └───────────────┘  └────────────────────┘  └─┘  └┘
642  
643  lemma mem_a_e_iff (s : set α) : s ∈ μ.a_e.sets ↔ μ (- s) = 0 := iff.rfl
id                          └─┘       └──┘└───┘             └─────┘
src                         └─┘          └──┘└───┘               └─────┘
typ                         └─┘       └──┘└───┘             └─────┘
doc                                       └──┘
644  
645  end measure
646  
647  end measure_theory
648  
649  section is_complete
650  open measure_theory
651  
652  variables {α : Type*} [measurable_space α] (μ : measure α)
id                         └──────────────┘         └─────┘
src                         └──────────────┘         └─────┘
typ                        └──────────────┘         └─────┘
653  
654  def is_null_measurable (s : set α) : Prop :=
id                               └─┘ 
src                              └─┘
typ                              └─┘ 
655  ∃ t z, s = t ∪ z ∧ is_measurable t ∧ μ z = 0
id            └───────────┘     
src                └───────────┘        
typ           └───────────┘     
doc                     └───────────┘
656  
657  theorem is_null_measurable_iff {μ : measure α} {s : set α} :
id                                       └─────┘        └─┘ 
src                                      └─────┘         └─┘
typ                                      └─────┘        └─┘ 
658    is_null_measurable μ s ↔
id     └────────────────┘   
src    └────────────────┘     
typ    └────────────────┘   
659    ∃ t, t ⊆ s ∧ is_measurable t ∧ μ (s \ t) = 0 :=
id           └───────────┘         
src             └───────────┘             
typ          └───────────┘         
doc                 └───────────┘
660  begin
st   └─────
661    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
662    { rintro ⟨t, z, rfl, ht, hz⟩,
src      └────────────────────────┘
typ      └────────────────────────┘
doc      └────────────────────────┘
txt      └────────────────────────┘
par      └────────────────────────┘
pid            └──────────────────┘
st   ───┘└────────────────────────┘└─
663      refine ⟨t, set.subset_union_left _ _, ht, measure_mono_null _ hz⟩,
id                 └───────────────────┘      └┘  └───────────────┘   └┘
src      └─────┘  └┘└───────────────────┘└────┘  └┘└───────────────┘└─┘  
typ      └─────┘ └┘└───────────────────┘└────┘└┘└┘└───────────────┘└─┘└┘
doc      └─────┘  └┘                     └────┘  └┘                 └─┘  
txt      └─────┘  └┘                     └────┘  └┘                 └─┘  
par      └─────┘  └┘                     └────┘  └┘                 └─┘  
pid              └┘                     └────┘  └┘                 └─┘  
st   ────────────────────────────────────────────────────────────────────┘└─
664      simp [union_diff_left, diff_subset] },
id             └─────────────┘  └─────────┘
src      └────┘└─────────────┘└┘└─────────┘└┘
typ      └────┘└─────────────┘└┘└─────────┘└┘
doc      └────┘               └┘           └┘
txt      └────┘               └┘           └┘
par      └────┘               └┘           └┘
pid                         └┘           
st   ───────────────────────────────────────┘└┘
665    { rintro ⟨t, st, ht, hz⟩,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid            └──────────────┘
st   ─────────────────────────┘└─
666      exact ⟨t, _, (union_diff_cancel st).symm, ht, hz⟩ }
id                    └───────────────┘ └┘        └┘  └┘
src      └────┘  └───┘ └───────────────┘  └──────┘  └┘  └┘
typ      └────┘ └───┘ └───────────────┘└┘└──────┘└┘└┘└┘└┘
doc      └────┘  └───┘                    └──────┘  └┘  └┘
txt      └────┘  └───┘                    └──────┘  └┘  └┘
par      └────┘  └───┘                    └──────┘  └┘  └┘
pid             └───┘                    └──────┘  └┘  
st   ─────────────────────────────────────────────────────┘└─
667  end
st   ──┘
668  
669  theorem is_null_measurable_measure_eq {μ : measure α} {s t : set α}
id                                              └─────┘          └─┘ 
src                                             └─────┘           └─┘
typ                                             └─────┘          └─┘ 
670    (st : t ⊆ s) (hz : μ (s \ t) = 0) : μ s = μ t :=
id                                     
src                                         
typ                                    
671  begin
st   └─────
672    refine le_antisymm _ (measure_mono st),
id            └─────────┘    └──────────┘ └┘
src    └─────┘└─────────┘└─┘ └──────────┘  
typ    └─────┘└─────────┘└─┘ └──────────┘└┘
doc    └─────┘           └─┘               
txt    └─────┘           └─┘               
par    └─────┘           └─┘               
pid                     └─┘               
st   ───────────────────────────────────────┘└─
673    have := measure_union_le t (s \ t),
id             └──────────────┘      
src    └──────┘└──────────────┘    
typ    └──────┘└──────────────┘  
doc    └──────┘                     
txt    └──────┘                     
par    └──────┘                     
pid    └───┘└─┘                     
st   ───────────────────────────────────┘└─
674    rw [union_diff_cancel st, hz] at this, simpa
id         └───────────────┘ └┘  └┘
src    └──┘└───────────────┘  └┘  └───────┘  └────┘
typ    └──┘└───────────────┘└┘└┘└┘└───────┘  └────┘
doc    └──┘                   └┘  └───────┘  └────┘
txt    └──┘                   └┘  └───────┘  └────┘
par    └──┘                   └┘  └───────┘  └────┘
pid      └┘                   └┘  └──────┘       
st   ─────────────────────────┘└──┘└──────┘└──────┘
675  end
st   └─┘
676  
677  theorem is_measurable.is_null_measurable
678    {s : set α} (hs : is_measurable s) : is_null_measurable μ s :=
id          └─┘         └───────────┘     └────────────────┘  
src         └─┘          └───────────┘      └────────────────┘
typ         └─┘         └───────────┘     └────────────────┘  
doc                      └───────────┘
679  ⟨s, ∅, by simp, hs, μ.empty⟩
id                 └┘  └────┘
src           └──┘       └────┘
typ          └──┘  └┘  └────┘
doc            └──┘
txt            └──┘
par            └──┘
st            └───┘
680  
681  theorem is_null_measurable_of_complete [c : μ.is_complete]
id                                               └──────────┘
src                                               └──────────┘
typ                                              └──────────┘
682    {s : set α} : is_null_measurable μ s ↔ is_measurable s :=
id          └─┘     └────────────────┘    └───────────┘ 
src         └─┘      └────────────────┘      └───────────┘
typ         └─┘     └────────────────┘    └───────────┘ 
doc                                           └───────────┘
683  ⟨by rintro ⟨t, z, rfl, ht, hz⟩; exact
src      └────────────────────────┘  └─────
typ      └────────────────────────┘  └─────
doc      └────────────────────────┘  └─────
txt      └────────────────────────┘  └─────
par      └────────────────────────┘  └─────
pid            └──────────────────┘       
st      └──────────────────────────────────
684    is_measurable.union ht (c _ hz),
id     └─────────────────┘ └┘     └┘
src  ─┘└─────────────────┘    └─┘  
typ  ─┘└─────────────────┘└┘ └─┘└┘
doc  ─┘                       └─┘  
txt  ─┘                       └─┘  
par  ─┘                       └─┘  
pid  ─┘                       └─┘  
st   ────────────────────────────────┘
685   λ h, h.is_null_measurable _⟩
id        └─────────────────┘
src         └─────────────────┘
typ       └─────────────────┘
686  
687  variables {μ}
688  theorem is_null_measurable.union_null {s z : set α}
id                                                └─┘ 
src                                               └─┘
typ                                               └─┘ 
689    (hs : is_null_measurable μ s) (hz : μ z = 0) :
id           └────────────────┘            
src          └────────────────┘                
typ          └────────────────┘            
690    is_null_measurable μ (s ∪ z) :=
id     └────────────────┘     
src    └────────────────┘      
typ    └────────────────┘     
691  begin
st   └─────
692    rcases hs with ⟨t, z', rfl, ht, hz'⟩,
id            └┘
src    └─────┘  └─────────────────────────┘
typ    └─────┘└┘└─────────────────────────┘
doc    └─────┘  └─────────────────────────┘
txt    └─────┘  └─────────────────────────┘
par    └─────┘  └─────────────────────────┘
pid            └─────────────────────────┘
st   ─────────────────────────────────────┘└─
693    exact ⟨t, z' ∪ z, set.union_assoc _ _ _, ht, le_zero_iff_eq.1
id              └┘    └─────────────┘        └┘  └────────────┘
src    └────┘  └┘   └┘└─────────────┘└──────┘  └┘└────────────┘└──
typ    └────┘ └┘└┘└┘└─────────────┘└──────┘└┘└┘└────────────┘└──
doc    └────┘  └┘    └┘               └──────┘  └┘              └──
txt    └────┘  └┘    └┘               └──────┘  └┘              └──
par    └────┘  └┘    └┘               └──────┘  └┘              └──
pid           └┘    └┘               └──────┘  └┘              └──
st   ────────────────────────────────────────────────────────────────
694      (le_trans (measure_union_le _ _) $ by simp [hz, hz'])⟩
id        └──────┘  └──────────────┘                 └┘  └─┘
src  ───┘ └──────┘ └──────────────┘└────┘   └────┘  └┘   └─┘
typ  ───┘ └──────┘ └──────────────┘└────┘   └────┘└┘└┘└─┘└─┘
doc  ───┘                          └────┘   └────┘  └┘   └─┘
txt  ───┘                          └────┘   └────┘  └┘   └─┘
par  ───┘                          └────┘   └────┘  └┘   └─┘
pid  ───┘                          └────┘   └─────┘  └┘   └─┘
st   ────────────────────────────────────────┘└─────────────┘└─┘
695  end
st   └─┘
696  
697  theorem null_is_null_measurable {z : set α}
id                                        └─┘ 
src                                       └─┘
typ                                       └─┘ 
698    (hz : μ z = 0) : is_null_measurable μ z :=
id                   └────────────────┘  
src                    └────────────────┘
typ                  └────────────────┘  
699  by simpa using (is_measurable.empty.is_null_measurable _).union_null hz
id                   └────────────────────────────────────┘               └┘
src     └──────────┘ └────────────────────────────────────┘└─────────────┘  
typ     └──────────┘ └────────────────────────────────────┘└─────────────┘└┘
doc     └──────────┘                                       └─────────────┘  
txt     └──────────┘                                       └─────────────┘  
par     └──────────┘                                       └─────────────┘  
pid          └────┘                                       └─────────────┘  
st     └─────────────────────────────────────────────────────────────────────
700  
src  
typ  
doc  
txt  
par  
pid  
st   
701  theorem is_null_measurable.Union_nat {s : ℕ → set α}
id                                                └─┘ 
src                                               └─┘
typ                                               └─┘ 
702    (hs : ∀ i, is_null_measurable μ (s i)) :
id               └────────────────┘    
src               └────────────────┘
typ              └────────────────┘    
703    is_null_measurable μ (Union s) :=
id     └────────────────┘   └───┘ 
src    └────────────────┘    └───┘
typ    └────────────────┘   └───┘ 
doc                          └───┘
704  begin
st   └─────
705    choose t ht using assume i, is_null_measurable_iff.1 (hs i),
id                                 └────────────────────┘    └┘
src    └────────────────┘      └──┘└────────────────────┘└─┘    
typ    └────────────────┘      └──┘└────────────────────┘└─┘ └┘ 
doc    └────────────────┘      └──┘                      └─┘    
txt    └────────────────┘      └──┘                      └─┘    
par    └────────────────┘      └──┘                      └─┘    
pid          └┘└─┘└─────┘      └──┘                      └─┘    
st   ────────────────────────────────────────────────────────────┘└─
706    simp [forall_and_distrib] at ht,
id           └────────────────┘
src    └────┘└────────────────┘└─────┘
typ    └────┘└────────────────┘└─────┘
doc    └────┘                  └─────┘
txt    └────┘                  └─────┘
par    └────┘                  └─────┘
pid                          └───┘
st   ────────────────────────────────┘└─
707    rcases ht with ⟨st, ht, hz⟩,
id            └┘
src    └─────┘  └────────────────┘
typ    └─────┘└┘└────────────────┘
doc    └─────┘  └────────────────┘
txt    └─────┘  └────────────────┘
par    └─────┘  └────────────────┘
pid            └────────────────┘
st   ────────────────────────────┘└─
708    refine is_null_measurable_iff.2
id            └────────────────────┘
src    └─────┘└────────────────────┘└──
typ    └─────┘└────────────────────┘└──
doc    └─────┘                      └──
txt    └─────┘                      └──
par    └─────┘                      └──
pid                                └──
st   ──────────────────────────────────
709      ⟨Union t, Union_subset_Union st, is_measurable.Union ht,
id        └───┘   └────────────────┘ └┘  └─────────────────┘ └┘
src  ───┘ └───┘ └┘└────────────────┘  └┘└─────────────────┘  └─
typ  ───┘ └───┘└┘└────────────────┘└┘└┘└─────────────────┘└┘└─
doc  ───┘ └───┘ └┘                    └┘                     └─
txt  ───┘       └┘                    └┘                     └─
par  ───┘       └┘                    └┘                     └─
pid  ───┘       └┘                    └┘                     └─
st   ─────────────────────────────────────────────────────────────
710        measure_mono_null _ (measure_Union_null hz)⟩,
id         └───────────────┘    └────────────────┘ └┘
src  ─────┘└───────────────┘└─┘ └────────────────┘  └┘
typ  ─────┘└───────────────┘└─┘ └────────────────┘└┘└┘
doc  ─────┘                 └─┘                     └┘
txt  ─────┘                 └─┘                     └┘
par  ─────┘                 └─┘                     └┘
pid  ─────┘                 └─┘                     └┘
st   ─────────────────────────────────────────────────┘└─
711    rw [diff_subset_iff, ← Union_union_distrib],
id         └─────────────┘    └─────────────────┘
src    └──┘└─────────────┘└──┘└─────────────────┘
typ    └──┘└─────────────┘└──┘└─────────────────┘
doc    └──┘               └──┘                   
txt    └──┘               └──┘                   
par    └──┘               └──┘                   
pid      └┘               └──┘                   
st   ────────────────────┘└─────────────────────┘└──
712    exact Union_subset_Union (λ i, by rw ← diff_subset_iff)
id           └────────────────┘               └─────────────┘
src    └────┘└────────────────┘  └──┘  └───┘└─────────────┘└┘
typ    └────┘└────────────────┘  └──┘  └───┘└─────────────┘└┘
doc    └────┘                    └──┘  └───┘               └┘
txt    └────┘                    └──┘  └───┘               └┘
par    └────┘                    └──┘  └───┘               └┘
pid                             └──┘  └────┘               
st   ──────────────────────────────────┘└───────────────────┘└┘
713  end
st   └─┘
714  
715  theorem is_measurable.diff_null {s z : set α}
id                                          └─┘ 
src                                         └─┘
typ                                         └─┘ 
716    (hs : is_measurable s) (hz : μ z = 0) :
id           └───────────┘           
src          └───────────┘              
typ          └───────────┘           
doc          └───────────┘
717    is_null_measurable μ (s \ z) :=
id     └────────────────┘     
src    └────────────────┘      
typ    └────────────────┘     
718  begin
st   └─────
719    rw measure_eq_infi at hz,
id        └─────────────┘
src    └─┘└─────────────┘└────┘
typ    └─┘└─────────────┘└────┘
doc    └─┘               └────┘
txt    └─┘               └────┘
par    └─┘               └────┘
pid                     └────┘
st   ─────────────────────────┘└─
720    choose f hf using show ∀ q : {q:ℚ//q>0}, ∃ t:set α,
id                                              └─┘ 
src    └────────────────┘     └───┘└┘└┘ └┘ └─┘└─┘ 
typ    └────────────────┘     └───┘└┘└┘ └┘ └─┘└─┘
doc    └────────────────┘     └───┘ └┘└┘  └┘  └─┘     
txt    └────────────────┘     └───┘ └┘ └┘  └┘  └─┘     
par    └────────────────┘     └───┘ └┘ └┘  └┘  └─┘     
pid          └┘└─┘└─────┘     └───┘ └┘ └┘  └┘  └─┘     
st   ──────────────────────────────────────────────────────
721      z ⊆ t ∧ is_measurable t ∧ μ t < (nnreal.of_real q.1 : ennreal),
id            └───────────┘          └────────────┘       └─────┘
src  ───┘  └───────────┘     └────────────┘ └───┘└─────┘└──
typ  ───┘ └───────────┘    └────────────┘ └───┘└─────┘└──
doc  ───┘    └───────────┘                     └───┘└─────┘└──
txt  ───┘                                      └───┘       └──
par  ───┘                                      └───┘       └──
pid  ───┘                                      └───┘       └──
st   ────────────────────────────────────────────────────────────────────
722    { rintro ⟨ε, ε0⟩,
src  ───┘└────────────┘└─
typ  ───┘└────────────┘└─
doc  ───┘└────────────┘└─
txt  ───┘└────────────┘└─
par  ───┘└────────────┘└─
pid  ────────────────────
st   ──┘└─────────────┘└─
723      have : 0 < (nnreal.of_real ε : ennreal), { simpa using ε0 },
id                   └────────────┘    └─────┘                 └┘
src  ───┘└───────┘  └────────────┘ └─┘└─────┘└──┘└──────────┘  └──
typ  ───┘└───────┘  └────────────┘└─┘└─────┘└──┘└──────────┘└┘└──
doc  ───┘└───────┘                 └─┘└─────┘└──┘└──────────┘  └──
txt  ───┘└───────┘                 └─┘       └──┘└──────────┘  └──
par  ───┘└───────┘                 └─┘       └──┘└──────────┘  └──
pid  ────────────┘                 └─┘       └───────────────┘  └───
st   ──────────────────────────────────────────┘└─┘└──────────────┘└─
724      rw ← hz at this, simpa [infi_lt_iff] },
id            └┘                 └─────────┘
src  ───┘└───┘  └──────┘└┘└─────┘└─────────┘└┘
typ  ───┘└───┘└┘└──────┘└┘└─────┘└─────────┘└┘
doc  ───┘└───┘  └──────┘└┘└─────┘           └┘
txt  ───┘└───┘  └──────┘└┘└─────┘           └┘
par  ───┘└───┘  └──────┘└┘└─────┘           └┘
pid  ────────┘  └───────────────┘           └─┘
st   ──────────────────┘└────────────────────┘└┘
725    refine is_null_measurable_iff.2 ⟨s \ Inter f,
id            └────────────────────┘      └───┘ 
src    └─────┘└────────────────────┘└─┘  └───┘ └─
typ    └─────┘└────────────────────┘└─┘ └───┘└─
doc    └─────┘                      └─┘   └───┘ └─
txt    └─────┘                      └─┘         └─
par    └─────┘                      └─┘         └─
pid                                └─┘         └─
st   ────────────────────────────────────────────────
726      diff_subset_diff_right (subset_Inter (λ i, (hf i).1)),
id       └────────────────────┘  └──────────┘
src  ───┘└────────────────────┘ └──────────┘  └──┘    └──────
typ  ───┘└────────────────────┘ └──────────┘  └──┘    └──────
doc  ───┘                                     └──┘    └──────
txt  ───┘                                     └──┘    └──────
par  ───┘                                     └──┘    └──────
pid  ───┘                                     └──┘    └──────
st   ───────────────────────────────────────────────────────────
727      hs.diff (is_measurable.Inter (λ i, (hf i).2.1)),
id       └─────┘  └─────────────────┘        └┘
src  ───┘└─────┘ └─────────────────┘  └──┘    └────────
typ  ───┘└─────┘ └─────────────────┘  └──┘ └┘ └────────
doc  ───┘                             └──┘    └────────
txt  ───┘                             └──┘    └────────
par  ───┘                             └──┘    └────────
pid  ───┘                             └──┘    └────────
st   ─────────────────────────────────────────────────────
728      measure_mono_null _ (le_zero_iff_eq.1 $ le_of_not_lt $ λ h, _)⟩,
id       └───────────────┘    └────────────┘     └──────────┘
src  ───┘└───────────────┘└─┘ └────────────┘└─┘ └──────────┘  └─────┘
typ  ───┘└───────────────┘└─┘ └────────────┘└─┘ └──────────┘  └─────┘
doc  ───┘                 └─┘               └─┘               └─────┘
txt  ───┘                 └─┘               └─┘               └─────┘
par  ───┘                 └─┘               └─┘               └─────┘
pid  ───┘                 └─┘               └─┘               └─────┘
st   ──────────────────────────────────────────────────────────────────┘└─
729    { exact Inter f },
id             └───┘ 
src      └────┘└───┘ 
typ      └────┘└───┘
doc      └────┘└───┘ 
txt      └────┘      
par      └────┘      
pid                 
st   ───┘└────────────┘└┘
730    { rw [diff_subset_iff, diff_union_self],
id           └─────────────┘  └─────────────┘
src      └──┘└─────────────┘└┘└─────────────┘
typ      └──┘└─────────────┘└┘└─────────────┘
doc      └──┘               └┘               
txt      └──┘               └┘               
par      └──┘               └┘               
pid        └┘               └┘               
st   ───┘└─────────────────┘└───────────────┘└──
731      exact subset.trans (diff_subset _ _) (subset_union_left _ _) },
id             └──────────┘  └─────────┘       └───────────────┘
src      └────┘└──────────┘ └─────────┘└────┘ └───────────────┘└────┘
typ      └────┘└──────────┘ └─────────┘└────┘ └───────────────┘└────┘
doc      └────┘                        └────┘                  └────┘
txt      └────┘                        └────┘                  └────┘
par      └────┘                        └────┘                  └────┘
pid                                   └────┘                  └───┘
st   ────────────────────────────────────────────────────────────────┘└┘
732    rcases ennreal.lt_iff_exists_rat_btwn.1 h with ⟨ε, ε0', ε0, h⟩,
id            └────────────────────────────┘   
src    └─────┘└────────────────────────────┘└─┘ └───────────────────┘
typ    └─────┘└────────────────────────────┘└─┘└───────────────────┘
doc    └─────┘                              └─┘ └───────────────────┘
txt    └─────┘                              └─┘ └───────────────────┘
par    └─────┘                              └─┘ └───────────────────┘
pid                                        └─┘ └───────────────────┘
st   ───────────────────────────────────────────────────────────────┘└─
733    simp at ε0,
src    └────────┘
typ    └────────┘
doc    └────────┘
txt    └────────┘
par    └────────┘
pid        └───┘
st   ───────────┘└─
734    apply not_le_of_lt (lt_trans (hf ⟨ε, ε0⟩).2.2 h),
id           └──────────┘  └──────┘  └┘    └┘       
src    └────┘└──────────┘ └──────┘     └┘  └─────┘ 
typ    └────┘└──────────┘ └──────┘ └┘ └┘└┘└─────┘
doc    └────┘                          └┘  └─────┘ 
txt    └────┘                          └┘  └─────┘ 
par    └────┘                          └┘  └─────┘ 
pid                                   └┘  └─────┘ 
st   ─────────────────────────────────────────────────┘└─
735    exact measure_mono (Inter_subset _ _)
id           └──────────┘  └──────────┘
src    └────┘└──────────┘ └──────────┘└────┘
typ    └────┘└──────────┘ └──────────┘└────┘
doc    └────┘                         └────┘
txt    └────┘                         └────┘
par    └────┘                         └────┘
pid                                  └───┘
st   ───────────────────────────────────────┘
736  end
st   └─┘
737  
738  theorem is_null_measurable.diff_null {s z : set α}
id                                               └─┘ 
src                                              └─┘
typ                                              └─┘ 
739    (hs : is_null_measurable μ s) (hz : μ z = 0) :
id           └────────────────┘            
src          └────────────────┘                
typ          └────────────────┘            
740    is_null_measurable μ (s \ z) :=
id     └────────────────┘     
src    └────────────────┘      
typ    └────────────────┘     
741  begin
st   └─────
742    rcases hs with ⟨t, z', rfl, ht, hz'⟩,
id            └┘
src    └─────┘  └─────────────────────────┘
typ    └─────┘└┘└─────────────────────────┘
doc    └─────┘  └─────────────────────────┘
txt    └─────┘  └─────────────────────────┘
par    └─────┘  └─────────────────────────┘
pid            └─────────────────────────┘
st   ─────────────────────────────────────┘└─
743    rw [set.union_diff_distrib],
id         └────────────────────┘
src    └──┘└────────────────────┘
typ    └──┘└────────────────────┘
doc    └──┘                      
txt    └──┘                      
par    └──┘                      
pid      └┘                      
st   ───────────────────────────┘└──
744    exact (ht.diff_null hz).union_null (measure_mono_null (diff_subset _ _) hz')
id            └──────────┘ └┘              └───────────────┘  └─────────┘      └─┘
src    └────┘ └──────────┘  └───────────┘ └───────────────┘ └─────────┘└────┘   └┘
typ    └────┘ └──────────┘└┘└───────────┘ └───────────────┘ └─────────┘└────┘└─┘└┘
doc    └────┘               └───────────┘                              └────┘   └┘
txt    └────┘               └───────────┘                              └────┘   └┘
par    └────┘               └───────────┘                              └────┘   └┘
pid                        └───────────┘                              └────┘   
st   ──────────────────────────────────────────────────────────────────────────────┘
745  end
st   └─┘
746  
747  theorem is_null_measurable.compl {s : set α}
id                                         └─┘ 
src                                        └─┘
typ                                        └─┘ 
748    (hs : is_null_measurable μ s) :
id           └────────────────┘  
src          └────────────────┘
typ          └────────────────┘  
749    is_null_measurable μ (-s) :=
id     └────────────────┘   
src    └────────────────┘    
typ    └────────────────┘   
750  begin
st   └─────
751    rcases hs with ⟨t, z, rfl, ht, hz⟩,
id            └┘
src    └─────┘  └───────────────────────┘
typ    └─────┘└┘└───────────────────────┘
doc    └─────┘  └───────────────────────┘
txt    └─────┘  └───────────────────────┘
par    └─────┘  └───────────────────────┘
pid            └───────────────────────┘
st   ───────────────────────────────────┘└─
752    rw compl_union,
id        └─────────┘
src    └─┘└─────────┘
typ    └─┘└─────────┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ───────────────┘└─
753    exact ht.compl.diff_null hz
id           └────────────────┘ └┘
src    └────┘└────────────────┘  
typ    └────┘└────────────────┘└┘
doc    └────┘                    
txt    └────┘                    
par    └────┘                    
pid                             
st   ─────────────────────────────┘
754  end
st   └─┘
755  
756  def null_measurable {α : Type u} [measurable_space α]
id                                     └──────────────┘ 
src                                    └──────────────┘
typ                                    └──────────────┘ 
757    (μ : measure α) : measurable_space α :=
id          └─────┘     └──────────────┘ 
src         └─────┘      └──────────────┘
typ         └─────┘     └──────────────┘ 
758  { is_measurable := is_null_measurable μ,
id                      └────────────────┘ 
src                     └────────────────┘
typ                     └────────────────┘ 
759    is_measurable_empty := is_measurable.empty.is_null_measurable _,
id                            └─────────────────┘└─────────────────┘
src                           └─────────────────┘└─────────────────┘
typ                           └─────────────────┘└─────────────────┘
760    is_measurable_compl := λ s hs, hs.compl,
id                               └┘  └┘└────┘
src                                     └────┘
typ                              └┘  └┘└────┘
761    is_measurable_Union := λ f, is_null_measurable.Union_nat }
id                                └──────────────────────────┘
src                                └──────────────────────────┘
typ                               └──────────────────────────┘
762  
763  def completion {α : Type u} [measurable_space α] (μ : measure α) :
id                                └──────────────┘        └─────┘ 
src                               └──────────────┘         └─────┘
typ                               └──────────────┘        └─────┘ 
764    @measure_theory.measure α (null_measurable μ) :=
id      └────────────────────┘   └─────────────┘ 
src     └────────────────────┘    └─────────────┘
typ     └────────────────────┘   └─────────────┘ 
765  { to_outer_measure := μ.to_outer_measure,
id                         └───────────────┘
src                         └───────────────┘
typ                        └───────────────┘
766    m_Union := λ s hs hd, show μ (Union s) = ∑ i, μ (s i), begin
id                   └┘ └┘         └───┘         
src                                  └───┘       
typ                  └┘ └┘         └───┘         
doc                                  └───┘        
st                                                            └─────
767      choose t ht using assume i, is_null_measurable_iff.1 (hs i),
id                                   └────────────────────┘    └┘
src      └────────────────┘      └──┘└────────────────────┘└─┘    
typ      └────────────────┘      └──┘└────────────────────┘└─┘ └┘ 
doc      └────────────────┘      └──┘                      └─┘    
txt      └────────────────┘      └──┘                      └─┘    
par      └────────────────┘      └──┘                      └─┘    
pid            └┘└─┘└─────┘      └──┘                      └─┘    
st   ──────────────────────────────────────────────────────────────┘└─
768      simp [forall_and_distrib] at ht, rcases ht with ⟨st, ht, hz⟩,
id             └────────────────┘                └┘
src      └────┘└────────────────┘└─────┘  └─────┘  └────────────────┘
typ      └────┘└────────────────┘└─────┘  └─────┘└┘└────────────────┘
doc      └────┘                  └─────┘  └─────┘  └────────────────┘
txt      └────┘                  └─────┘  └─────┘  └────────────────┘
par      └────┘                  └─────┘  └─────┘  └────────────────┘
pid                            └───┘          └────────────────┘
st   ──────────────────────────────────┘└───────────────────────────┘└─
769      rw is_null_measurable_measure_eq (Union_subset_Union st),
id          └───────────────────────────┘  └────────────────┘ └┘
src      └─┘└───────────────────────────┘ └────────────────┘  
typ      └─┘└───────────────────────────┘ └────────────────┘└┘
doc      └─┘                                                  
txt      └─┘                                                  
par      └─┘                                                  
pid                                                          
st   ───────────────────────────────────────────────────────────┘└─
770      { rw measure_Union _ ht,
id            └───────────┘   └┘
src        └─┘└───────────┘└─┘
typ        └─┘└───────────┘└─┘└┘
doc        └─┘             └─┘
txt        └─┘             └─┘
par        └─┘             └─┘
pid                       └─┘
st   ─────┘└───────────────────┘└─
771        { congr, funext i,
src          └───┘  └──────┘
typ          └───┘  └──────┘
doc                 └──────┘
txt          └───┘  └──────┘
par          └───┘  └──────┘
pid                       └┘
st   ───────┘└───┘└────────┘└─
772          exact (is_null_measurable_measure_eq (st i) (hz i)).symm },
id                  └───────────────────────────┘  └┘     └┘ 
src          └────┘ └───────────────────────────┘    └┘    └──────┘
typ          └────┘ └───────────────────────────┘ └┘ └┘ └┘└──────┘
doc          └────┘                                  └┘    └──────┘
txt          └────┘                                  └┘    └──────┘
par          └────┘                                  └┘    └──────┘
pid                                                 └┘    └────┘└┘
st   ────────────────────────────────────────────────────────────────┘└┘
773        { rintro i j ij x ⟨h₁, h₂⟩,
src          └──────────────────────┘
typ          └──────────────────────┘
doc          └──────────────────────┘
txt          └──────────────────────┘
par          └──────────────────────┘
pid                └────────────────┘
st   ───────────────────────────────┘└─
774          exact hd i j ij ⟨st i h₁, st j h₂⟩ } },
id                 └┘     └┘      └┘  └┘  └┘
src          └────┘            └┘     └┘
typ          └────┘└┘  └┘   └┘└┘└┘└┘└┘
doc          └────┘            └┘     └┘
txt          └────┘            └┘     └┘
par          └────┘            └┘     └┘
pid                           └┘     
st   ──────────────────────────────────────────┘└──┘
775      { refine measure_mono_null _ (measure_Union_null hz),
id                └───────────────┘    └────────────────┘ └┘
src        └─────┘└───────────────┘└─┘ └────────────────┘  
typ        └─────┘└───────────────┘└─┘ └────────────────┘└┘
doc        └─────┘                 └─┘                     
txt        └─────┘                 └─┘                     
par        └─────┘                 └─┘                     
pid                               └─┘                     
st   ───────────────────────────────────────────────────────┘└─
776        rw [diff_subset_iff, ← Union_union_distrib],
id             └─────────────┘    └─────────────────┘
src        └──┘└─────────────┘└──┘└─────────────────┘
typ        └──┘└─────────────┘└──┘└─────────────────┘
doc        └──┘               └──┘                   
txt        └──┘               └──┘                   
par        └──┘               └──┘                   
pid          └┘               └──┘                   
st   ────────────────────────┘└─────────────────────┘└──
777        exact Union_subset_Union (λ i, by rw ← diff_subset_iff) }
id               └────────────────┘               └─────────────┘
src        └────┘└────────────────┘  └──┘  └───┘└─────────────┘└┘
typ        └────┘└────────────────┘  └──┘  └───┘└─────────────┘└┘
doc        └────┘                    └──┘  └───┘               └┘
txt        └────┘                    └──┘  └───┘               └┘
par        └────┘                    └──┘  └───┘               └┘
pid                                 └──┘  └────┘               
st   ──────────────────────────────────────┘└───────────────────┘└┘└─
778    end,
st   ────┘
779    trimmed := begin
st                └─────
780      letI := null_measurable μ,
id               └─────────────┘ 
src      └──────┘└─────────────┘
typ      └──────┘└─────────────┘
doc      └──────┘               
txt      └──────┘               
par      └──────┘               
pid          └─┘               
st   ────────────────────────────┘└─
781      refine le_antisymm (λ s, _) (outer_measure.trim_ge _),
id              └─────────┘           └───────────────────┘
src      └─────┘└─────────┘  └─────┘ └───────────────────┘└─┘
typ      └─────┘└─────────┘  └─────┘ └───────────────────┘└─┘
doc      └─────┘             └─────┘                      └─┘
txt      └─────┘             └─────┘                      └─┘
par      └─────┘             └─────┘                      └─┘
pid                         └─────┘                      └─┘
st   ────────────────────────────────────────────────────────┘└─
782      rw outer_measure.trim_eq_infi,
id          └────────────────────────┘
src      └─┘└────────────────────────┘
typ      └─┘└────────────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ────────────────────────────────┘└─
783      dsimp, clear _inst,
src      └───┘  └─────────┘
typ      └───┘  └─────────┘
doc      └───┘  └─────────┘
txt      └───┘  └─────────┘
par      └───┘  └─────────┘
pid                  └────┘
st   ────────┘└───────────┘└─
784      rw measure_eq_infi s,
id          └─────────────┘ 
src      └─┘└─────────────┘
typ      └─┘└─────────────┘
doc      └─┘               
txt      └─┘               
par      └─┘               
pid                       
st   ───────────────────────┘└─
785      exact infi_le_infi (λ t, infi_le_infi $ λ st,
id                                └──────────┘
src      └────┘              └──┘└──────────┘  └────
typ      └────┘              └──┘└──────────┘  └────
doc      └────┘              └──┘              └────
txt      └────┘              └──┘              └────
par      └────┘              └──┘              └────
pid                         └──┘              └────
st   ──────────────────────────────────────────────────
786        infi_le_infi2 $ λ ht, ⟨ht.is_null_measurable _, le_refl _⟩)
id         └───────────┘            └─────────────────┘    └─────┘
src  ─────┘└───────────┘  └───┘   └─────────────────┘└──┘└─────┘└────
typ  ─────┘└───────────┘  └───┘   └─────────────────┘└──┘└─────┘└────
doc  ─────┘               └───┘                      └──┘       └────
txt  ─────┘               └───┘                      └──┘       └────
par  ─────┘               └───┘                      └──┘       └────
pid  ─────┘               └───┘                      └──┘       └──┘
st   ──────────────────────────────────────────────────────────────────
787    end }
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
788  
789  instance completion.is_complete {α : Type u} [measurable_space α] (μ : measure α) :
id                                                 └──────────────┘        └─────┘ 
src                                                └──────────────┘         └─────┘
typ                                                └──────────────┘        └─────┘ 
790    (completion μ).is_complete :=
id      └────────┘  └─────────┘
src     └────────┘   └─────────┘
typ     └────────┘  └─────────┘
791  λ z hz, null_is_null_measurable hz
id      └┘  └─────────────────────┘ └┘
src          └─────────────────────┘
typ     └┘  └─────────────────────┘ └┘
792  
793  end is_complete
794  
795  namespace measure_theory
796  
797  section prio
798  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
799  /-- A measure space is a measurable space equipped with a
800    measure, referred to as `volume`. -/
801  class measure_space (α : Type*) extends measurable_space α :=
id                            └───┘          └──────────────┘ 
src                                          └──────────────┘
typ                           └───┘          └──────────────┘ 
802  (μ {} : measure α)
id           └─────┘ 
src          └─────┘
typ          └─────┘ 
803  end prio
804  
805  section measure_space
806  variables {α : Type*} [measure_space α] {s₁ s₂ : set α}
id                         └───────────┘             └─┘
src                         └───────────┘             └─┘
typ                        └───────────┘             └─┘
doc                         └───────────┘
807  open measure_space
808  
809  def volume : set α → ennreal := @μ α _
id                └─┘    └─────┘      
src               └─┘     └─────┘     
typ               └─┘    └─────┘      
doc                       └─────┘
810  
811  @[simp] lemma volume_empty : volume (∅ : set α) = 0 := μ.empty
id                                └────┘     └─┘         └────┘
src                               └────┘     └─┘          └────┘
typ                               └────┘     └─┘         └────┘
doc    └──┘
812  
813  lemma volume_mono : s₁ ⊆ s₂ → volume s₁ ≤ volume s₂ := measure_mono
id                       └┘  └┘   └────┘ └┘  └────┘ └┘    └──────────┘
src                               └────┘     └────┘       └──────────┘
typ                      └┘  └┘   └────┘ └┘  └────┘ └┘    └──────────┘
814  
815  lemma volume_mono_null : s₁ ⊆ s₂ → volume s₂ = 0 → volume s₁ = 0 :=
id                            └┘  └┘   └────┘ └┘      └────┘ └┘ 
src                                    └────┘         └────┘    
typ                           └┘  └┘   └────┘ └┘      └────┘ └┘ 
816  measure_mono_null
id   └───────────────┘
src  └───────────────┘
typ  └───────────────┘
817  
818  theorem volume_Union_le {β} [encodable β] :
id                                └───────┘ 
src                               └───────┘
typ                               └───────┘ 
doc                               └───────┘
819    ∀ (s : β → set α), volume (⋃i, s i) ≤ (∑i, volume (s i)) :=
id              └─┘    └────┘         └────┘   
src               └─┘     └────┘             └────┘
typ             └─┘    └────┘         └────┘   
doc                                          
820  measure_Union_le
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
821  
822  lemma volume_Union_null {β} [encodable β] {s : β → set α} :
id                                └───────┘           └─┘ 
src                               └───────┘             └─┘
typ                               └───────┘           └─┘ 
doc                               └───────┘
823    (∀ i, volume (s i) = 0) → volume (⋃i, s i) = 0 :=
id          └────┘           └────┘      
src          └────┘             └────┘         
typ         └────┘           └────┘      
doc                                       
824  measure_Union_null
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
825  
826  theorem volume_union_le : ∀ (s₁ s₂ : set α), volume (s₁ ∪ s₂) ≤ volume s₁ + volume s₂ :=
id                                        └─┘    └────┘  └┘  └┘   └────┘ └┘  └────┘ └┘
src                                       └─┘     └────┘           └────┘     └────┘
typ                                       └─┘    └────┘  └┘  └┘   └────┘ └┘  └────┘ └┘
827  measure_union_le
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
828  
829  lemma volume_union_null : volume s₁ = 0 → volume s₂ = 0 → volume (s₁ ∪ s₂) = 0 :=
id                             └────┘ └┘      └────┘ └┘      └────┘  └┘  └┘  
src                            └────┘         └────┘         └────┘          
typ                            └────┘ └┘      └────┘ └┘      └────┘  └┘  └┘  
830  measure_union_null
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
831  
832  lemma volume_Union {β} [encodable β] {f : β → set α} :
id                           └───────┘           └─┘ 
src                          └───────┘             └─┘
typ                          └───────┘           └─┘ 
doc                          └───────┘
833    pairwise (disjoint on f) → (∀i, is_measurable (f i)) →
id     └──────┘  └──────┘ └┘         └───────────┘   
src    └──────┘  └──────┘ └┘           └───────────┘
typ    └──────┘  └──────┘ └┘         └───────────┘   
doc    └──────┘  └──────┘              └───────────┘
834    volume (⋃i, f i) = (∑i, volume (f i)) :=
id     └────┘         └────┘   
src    └────┘             └────┘
typ    └────┘         └────┘   
doc                       
835  measure_Union
id   └───────────┘
src  └───────────┘
typ  └───────────┘
836  
837  lemma volume_union : disjoint s₁ s₂ → is_measurable s₁ → is_measurable s₂ →
id                        └──────┘ └┘ └┘   └───────────┘ └┘   └───────────┘ └┘
src                       └──────┘         └───────────┘      └───────────┘
typ                       └──────┘ └┘ └┘   └───────────┘ └┘   └───────────┘ └┘
doc                       └──────┘         └───────────┘      └───────────┘
838    volume (s₁ ∪ s₂) = volume s₁ + volume s₂ :=
id     └────┘  └┘  └┘   └────┘ └┘  └────┘ └┘
src    └────┘           └────┘     └────┘
typ    └────┘  └┘  └┘   └────┘ └┘  └────┘ └┘
839  measure_union
id   └───────────┘
src  └───────────┘
typ  └───────────┘
840  
841  lemma volume_bUnion {β} {s : set β} {f : β → set α} : countable s →
id                                └─┘           └─┘     └───────┘ 
src                               └─┘             └─┘      └───────┘
typ                               └─┘           └─┘     └───────┘ 
doc                                                        └───────┘
842    pairwise_on s (disjoint on f) → (∀b∈s, is_measurable (f b)) →
id     └─────────┘   └──────┘ └┘          └───────────┘   
src    └─────────┘    └──────┘ └┘             └───────────┘
typ    └─────────┘   └──────┘ └┘          └───────────┘   
doc    └─────────┘    └──────┘                └───────────┘
843    volume (⋃b∈s, f b) = ∑p:s, volume (f p.1) :=
id     └────┘           └────┘   
src    └────┘                └────┘     
typ    └────┘           └────┘   
doc                          
844  measure_bUnion
id   └────────────┘
src  └────────────┘
typ  └────────────┘
845  
846  lemma volume_sUnion {S : set (set α)} : countable S →
id                            └─┘  └─┘      └───────┘ 
src                           └─┘  └─┘       └───────┘
typ                           └─┘  └─┘      └───────┘ 
doc                                          └───────┘
847    pairwise_on S disjoint → (∀s∈S, is_measurable s) →
id     └─────────┘  └──────┘        └───────────┘ 
src    └─────────┘   └──────┘          └───────────┘
typ    └─────────┘  └──────┘        └───────────┘ 
doc    └─────────┘   └──────┘          └───────────┘
848    volume (⋃₀ S) = ∑s:S, volume s.1 :=
id     └────┘  └┘       └────┘ 
src    └────┘  └┘         └────┘  
typ    └────┘  └┘       └────┘ 
doc                       
849  measure_sUnion
id   └────────────┘
src  └────────────┘
typ  └────────────┘
850  
851  lemma volume_bUnion_finset {β} {s : finset β} {f : β → set α}
id                                       └────┘           └─┘ 
src                                      └────┘             └─┘
typ                                      └────┘           └─┘ 
doc                                      └────┘
852    (hd : pairwise_on ↑s (disjoint on f)) (hm : ∀b∈s, is_measurable (f b)) :
id           └─────────┘   └──────┘ └┘              └───────────┘   
src          └─────────┘    └──────┘ └┘                 └───────────┘
typ          └─────────┘   └──────┘ └┘              └───────────┘   
doc          └─────────┘     └──────┘                    └───────────┘
853    volume (⋃b∈s, f b) = s.sum (λp, volume (f p)) :=
id     └────┘        └──┘     └────┘   
src    └────┘             └──┘      └────┘
typ    └────┘        └──┘     └────┘   
doc               
854  show volume (⋃b∈(↑s : set β), f b) = s.sum (λp, volume (f p)),
id        └────┘       └─┘       └──┘     └────┘   
src       └────┘         └─┘           └──┘      └────┘
typ       └────┘       └─┘       └──┘     └────┘   
doc                             
855  begin
st   └─────
856    rw [volume_bUnion (countable_finite (finset.finite_to_set s)) hd hm, tsum_eq_sum],
id         └───────────┘  └──────────────┘  └──────────────────┘    └┘ └┘  └─────────┘
src    └──┘└───────────┘ └──────────────┘ └──────────────────┘ └─┘    └┘└─────────┘
typ    └──┘└───────────┘ └──────────────┘ └──────────────────┘└─┘└┘└┘└┘└─────────┘
doc    └──┘                                                    └─┘    └┘           
txt    └──┘                                                    └─┘    └┘           
par    └──┘                                                    └─┘    └┘           
pid      └┘                                                    └─┘    └┘           
st   ────────────────────────────────────────────────────────────────────┘└───────────┘└──
857    { show s.attach.sum (λb:(↑s : set β), volume (f b)) = s.sum (λb, volume (f b)),
id            └──────────┘         └─┘                   └───┘      └────┘  
src      └───┘└──────────┘  └┘  └─┘└─┘ └─┘         └─┘└───┘  └─┘└────┘   └┘
typ      └───┘└──────────┘  └┘ └─┘└─┘└─┘         └─┘└───┘  └─┘└────┘  └┘
doc      └───┘└──────────┘  └┘   └─┘    └─┘         └─┘        └─┘         └┘
txt      └───┘              └┘   └─┘    └─┘         └─┘        └─┘         └┘
par      └───┘              └┘   └─┘    └─┘         └─┘        └─┘         └┘
pid      └───┘              └┘   └─┘    └─┘         └─┘        └─┘         └┘
st   ───┘└──────────────────────────────────────────────────────────────────────────┘└─
858      exact @finset.sum_attach _ _ s _ (λb, volume (f b)) },
id              └───────────────┘             └────┘  
src      └────┘ └───────────────┘└───┘ └─┘  └─┘└────┘   └─┘
typ      └────┘ └───────────────┘└───┘└─┘  └─┘└────┘  └─┘
doc      └────┘                  └───┘ └─┘  └─┘         └─┘
txt      └────┘                  └───┘ └─┘  └─┘         └─┘
par      └────┘                  └───┘ └─┘  └─┘         └─┘
pid                             └───┘ └─┘  └─┘         └┘
st   ───────────────────────────────────────────────────────┘└┘
859    simp
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
pid        
st   ──────┘
860  end
st   └─┘
861  
862  lemma volume_diff : s₂ ⊆ s₁ → is_measurable s₁ → is_measurable s₂ →
id                       └┘  └┘   └───────────┘ └┘   └───────────┘ └┘
src                               └───────────┘      └───────────┘
typ                      └┘  └┘   └───────────┘ └┘   └───────────┘ └┘
doc                                └───────────┘      └───────────┘
863    volume s₂ < ⊤ → volume (s₁ \ s₂) = volume s₁ - volume s₂ :=
id     └────┘ └┘     └────┘  └┘  └┘   └────┘ └┘  └────┘ └┘
src    └────┘        └────┘           └────┘     └────┘
typ    └────┘ └┘     └────┘  └┘  └┘   └────┘ └┘  └────┘ └┘
864  measure_diff
id   └──────────┘
src  └──────────┘
typ  └──────────┘
865  
866  /-- `∀ₘ a:α, p a` states that the property `p` is almost everywhere true in the measure space
867  associated with `α`. This means that the measure of the complementary of `p` is `0`.
868  
869  In a probability measure, the measure of `p` is `1`, when `p` is measurable.
870  -/
871  def all_ae (p : α → Prop) : Prop :=
id                   
typ                  
872  ∀ᶠ a in μ.a_e, p a
id   └┘  └┘ └──┘  
src  └┘   └┘ └──┘
typ  └┘  └┘ └──┘  
doc  └┘   └┘  └──┘
873  
874  notation `∀ₘ` binders `, ` r:(scoped P, all_ae P) := r
id                                           └────┘
src                                          └────┘
typ                                          └────┘
doc                                          └────┘
875  
876  lemma all_ae_congr {p q : α → Prop} (h : ∀ₘ a, p a ↔ q a) : (∀ₘ a, p a) ↔ (∀ₘ a, q a) :=
id                                           └┘           └┘       └┘   
src                                           └┘                └┘          └┘  
typ                                          └┘           └┘       └┘   
doc                                           └┘                 └┘           └┘  
877  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
878    (assume h', by filter_upwards [h, h'] assume a hpq hp, hpq.1 hp)
id             └┘
src                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
typ            └┘     └──────────────┘ └┘  └┘      └─────────┘   └─┘
doc                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
txt                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
par                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
pid                                 └┘ └┘        └─────────┘   └─┘
st                   └───────────────────────────────────────────────┘
879    (assume h', by filter_upwards [h, h'] assume a hpq hq, hpq.2 hq)
id             └┘
src                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
typ            └┘     └──────────────┘ └┘  └┘      └─────────┘   └─┘
doc                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
txt                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
par                   └──────────────┘ └┘  └┘      └─────────┘   └─┘
pid                                 └┘ └┘        └─────────┘   └─┘
st                   └───────────────────────────────────────────────┘
880  
881  lemma all_ae_iff {p : α → Prop} : (∀ₘ a, p a) ↔ volume { a | ¬ p a } = 0 := iff.rfl
id                                     └┘      └────┘                └─────┘
src                                     └┘         └────┘                   └─────┘
typ                                    └┘      └────┘                └─────┘
doc                                     └┘  
882  
883  lemma all_ae_of_all {p : α → Prop} : (∀a, p a) → ∀ₘ a, p a := univ_mem_sets'
id                                                └┘       └────────────┘
src                                                   └┘          └────────────┘
typ                                               └┘       └────────────┘
doc                                                   └┘  
884  
885  lemma all_ae_all_iff {ι : Type*} [encodable ι] {p : α → ι → Prop} :
id                                     └───────┘           
src                                    └───────┘
typ                                    └───────┘           
doc                                    └───────┘
886    (∀ₘ a, ∀i, p a i) ↔ (∀i, ∀ₘ a, p a i) :=
id      └┘              └┘    
src     └┘                    └┘  
typ     └┘              └┘    
doc     └┘                     └┘  
887  begin
st   └─────
888    refine iff.intro (assume h i, _) (assume h, _),
id            └───────┘
src    └─────┘└───────┘       └───────┘       └────┘
typ    └─────┘└───────┘       └───────┘       └────┘
doc    └─────┘                └───────┘       └────┘
txt    └─────┘                └───────┘       └────┘
par    └─────┘                └───────┘       └────┘
pid                          └───────┘       └────┘
st   ───────────────────────────────────────────────┘└─
889    { filter_upwards [h] assume a ha, ha i },
id                                          
src      └──────────────┘ └┘      └─────┘   
typ      └──────────────┘ └┘      └─────┘  
doc      └──────────────┘ └┘      └─────┘   
txt      └──────────────┘ └┘      └─────┘   
par      └──────────────┘ └┘      └─────┘   
pid                    └┘       └─────┘   
st   ───┘└───────────────────────────────────┘└┘
890    { have h := measure_Union_null h,
id                 └────────────────┘ 
src      └────────┘└────────────────┘
typ      └────────┘└────────────────┘
doc      └────────┘                  
txt      └────────┘                  
par      └────────┘                  
pid      └────┘└─┘                  
st   ─────────────────────────────────┘└─
891      rw [← compl_Inter] at h,
id             └─────────┘
src      └────┘└─────────┘└────┘
typ      └────┘└─────────┘└────┘
doc      └────┘           └────┘
txt      └────┘           └────┘
par      └────┘           └────┘
pid        └──┘           └───┘
st   ────────────────────┘└───┘└─
892      filter_upwards [h] assume a, mem_Inter.1 }
id                                    └───────┘
src      └──────────────┘ └┘      └──┘└───────┘└─┘
typ      └──────────────┘ └┘      └──┘└───────┘└─┘
doc      └──────────────┘ └┘      └──┘         └─┘
txt      └──────────────┘ └┘      └──┘         └─┘
par      └──────────────┘ └┘      └──┘         └─┘
pid                    └┘       └──┘         └─┘
st   ────────────────────────────────────────────┘└─
893  end
st   ──┘
894  
895  variables {β : Type*}
896  
897  lemma all_ae_eq_refl (f : α → β) : ∀ₘ a, f a = f a :=
id                                    └┘      
src                                     └┘       
typ                                   └┘      
doc                                     └┘  
898  by { filter_upwards [], assume a, apply eq.refl }
id                                           └─────┘
src       └───────────────┘  └──────┘  └────┘└─────┘
typ       └───────────────┘  └──────┘  └────┘└─────┘
doc       └───────────────┘  └──────┘  └────┘       
txt       └───────────────┘  └──────┘  └────┘       
par       └───────────────┘  └──────┘  └────┘       
pid                     └─┘  └──────┘              
st     └──────────────────┘└────────┘└──────────────┘└┘
899  
900  lemma all_ae_eq_symm {f g : α → β} : (∀ₘ a, f a = g a) → (∀ₘ a, g a = f a) :=
id                                       └┘           └┘      
src                                        └┘                └┘       
typ                                      └┘           └┘      
doc                                        └┘                 └┘  
901  by { assume h, filter_upwards [h], assume a, apply eq.symm }
id                                                      └─────┘
src       └──────┘  └──────────────┘   └──────┘  └────┘└─────┘
typ       └──────┘  └──────────────┘   └──────┘  └────┘└─────┘
doc       └──────┘  └──────────────┘   └──────┘  └────┘       
txt       └──────┘  └──────────────┘   └──────┘  └────┘       
par       └──────┘  └──────────────┘   └──────┘  └────┘       
pid       └──────┘                └┘   └──────┘              
st     └─────────┘└──────────────────┘└────────┘└──────────────┘└┘
902  
903  lemma all_ae_eq_trans {f g h: α → β} (h₁ : ∀ₘ a, f a = g a) (h₂ : ∀ₘ a, g a = h a) :
id                                            └┘              └┘      
src                                             └┘                   └┘       
typ                                           └┘              └┘      
doc                                             └┘                    └┘  
904    ∀ₘ a, f a = h a :=
id     └┘      
src    └┘       
typ    └┘      
doc    └┘  
905  by { filter_upwards [h₁, h₂], intro a, exact eq.trans }
id                                                └──────┘
src       └──────────────┘  └┘    └─────┘  └────┘└──────┘
typ       └──────────────┘  └┘    └─────┘  └────┘└──────┘
doc       └──────────────┘  └┘    └─────┘  └────┘        
txt       └──────────────┘  └┘    └─────┘  └────┘        
par       └──────────────┘  └┘    └─────┘  └────┘        
pid                     └┘  └┘         └┘               
st     └────────────────────────┘└───────┘└───────────────┘└┘
906  
907  end measure_space
908  
909  end measure_theory